THEOREM

*******

 

For every set x and y, there exists a set of graphs (ordered pairs), each of which corresponds a function mapping x to y.

 

   ALL(x):ALL(y):[Set(x) & Set(y)

   => EXIST(graphs):[Set(graphs)

   & ALL(g):[g e graphs

   <=> Set'(g)

   & ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

   & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

   & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y => [(a,b) e g & (a,c) e g => b=c]]]]

 

   & ALL(g):[g e graphs

   => EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y

   => [fun(a1)=b <=> (a1,b) e g]]]]]

 

The revised Function Axiom is used on line 82.

 

By Dan Christensen

2022-01-25

 

 

This machine-verfied, formal proof was written with the aid of the author's DC Proof 2.0 freeware available http://www.dcprof.com

 

PROOF

*****

 

    Let x and y be sets.

 

 

      1     Set(x) & Set(y)

            Premise

 

      2     Set(x)

            Split, 1

 

      3     Set(y)

            Split, 1

 

   

    Construct to set of all graphs mapping x to y

   

    Apply Cartesian Product Axiom

 

      4     ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]

            Cart Prod

 

      5     ALL(a2):[Set(x) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e a2]]]

            U Spec, 4

 

      6     Set(x) & Set(y) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e y]]

            U Spec, 5

 

      7     EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e y]]

            Detach, 6, 1

 

      8     Set'(xy) & ALL(c1):ALL(c2):[(c1,c2) e xy <=> c1 e x & c2 e y]

            E Spec, 7

 

    Define: xy  (Cartesian product of x and y)

 

      9     Set'(xy)

            Split, 8

 

      10   ALL(c1):ALL(c2):[(c1,c2) e xy <=> c1 e x & c2 e y]

            Split, 8

 

    Apply Power Set Axiom

 

      11   ALL(a):[Set'(a) => EXIST(b):[Set(b)

         & ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e a]]]]

            Power Set

 

      12   Set'(xy) => EXIST(b):[Set(b)

         & ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e xy]]]

            U Spec, 11

 

      13   EXIST(b):[Set(b)

         & ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e xy]]]

            Detach, 12, 9

 

      14   Set(pxy)

         & ALL(c):[c e pxy <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e xy]]

            E Spec, 13

 

    Define: pxy  (Power set of xy)

 

      15   Set(pxy)

            Split, 14

 

      16   ALL(c):[c e pxy <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e xy]]

            Split, 14

 

      17   EXIST(graphs):[Set(graphs) & ALL(g):[g e graphs <=> g e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

         & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

         => [(a,b) e g & (a,c) e g => b=c]]]]]

            Subset, 15

 

      18   Set(graphs) & ALL(g):[g e graphs <=> g e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

         & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

         => [(a,b) e g & (a,c) e g => b=c]]]]

            E Spec, 17

 

   

    Define: graphs  (Set of all graphs of functions mapping x to y)

 

      19   Set(graphs)

            Split, 18

 

      20   ALL(g):[g e graphs <=> g e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

         & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

         => [(a,b) e g & (a,c) e g => b=c]]]]

            Split, 18

 

        

         Elimainate pxy term

        

         '=>'

        

         Prove: ALL(g):[g e graphs

                => Set'(g)

                & ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

                & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

                & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

                => [(a,b) e g & (a,c) e g => b=c]]]]

        

         Suppose...

 

            21   g e graphs

                  Premise

 

            22   g e graphs <=> g e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]]

                  U Spec, 20

 

            23   [g e graphs => g e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]]]

             & [g e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]] => g e graphs]

                  Iff-And, 22

 

            24   g e graphs => g e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]]

                  Split, 23

 

            25   g e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]]

                  Detach, 24, 21

 

            26   g e pxy

                  Split, 25

 

            27   ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]

                  Split, 25

 

         Apply definition of pxy

 

            28   g e pxy <=> Set'(g) & ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy]

                  U Spec, 16

 

            29   [g e pxy => Set'(g) & ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy]]

             & [Set'(g) & ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy] => g e pxy]

                  Iff-And, 28

 

            30   g e pxy => Set'(g) & ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy]

                  Split, 29

 

            31   Set'(g) & ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy]

                  Detach, 30, 26

 

            32   Set'(g)

                  Split, 31

 

            33   ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy]

                  Split, 31

 

                  34   (t,u) e g

                        Premise

 

                  35   ALL(d2):[(t,d2) e g => (t,d2) e xy]

                        U Spec, 33

 

                  36   (t,u) e g => (t,u) e xy

                        U Spec, 35

 

                  37   (t,u) e xy

                        Detach, 36, 34

 

                  38   ALL(c2):[(t,c2) e xy <=> t e x & c2 e y]

                        U Spec, 10

 

                  39   (t,u) e xy <=> t e x & u e y

                        U Spec, 38

 

                  40   [(t,u) e xy => t e x & u e y]

                 & [t e x & u e y => (t,u) e xy]

                        Iff-And, 39

 

                  41   (t,u) e xy => t e x & u e y

                        Split, 40

 

                  42   t e x & u e y

                        Detach, 41, 37

 

            43   ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

                  4 Conclusion, 34

 

            44   Set'(g)

             & ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

                  Join, 32, 43

 

            45   Set'(g)

             & ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

             & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]]

                  Join, 44, 27

 

    As Required:

 

      46   ALL(g):[g e graphs

         => Set'(g)

         & ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

         & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

         & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

         => [(a,b) e g & (a,c) e g => b=c]]]]

            4 Conclusion, 21

 

        

         '<='

        

         Prove: ALL(g):[Set'(g)

                & ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

                & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

                & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

                => [(a,b) e g & (a,c) e g => b=c]]]

                => g e graphs]

        

         Suppose...

 

            47   Set'(g)

             & ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

             & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]]

                  Premise

 

            48   Set'(g)

                  Split, 47

 

            49   ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

                  Split, 47

 

            50   ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]

                  Split, 47

 

            51   g e graphs <=> g e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]]

                  U Spec, 20

 

            52   [g e graphs => g e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]]]

             & [g e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]] => g e graphs]

                  Iff-And, 51

 

         Sufficient: For g e graphs

 

            53   g e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]] => g e graphs

                  Split, 52

 

            54   g e pxy <=> Set'(g) & ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy]

                  U Spec, 16

 

            55   [g e pxy => Set'(g) & ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy]]

             & [Set'(g) & ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy] => g e pxy]

                  Iff-And, 54

 

         Sufficient: For g e pxy

 

            56   Set'(g) & ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy] => g e pxy

                  Split, 55

 

            

             Prove: ALL(a):ALL(b):[(a,b) e g => (a,b) e xy]

            

             Suppose...

 

                  57   (t,u) e g

                        Premise

 

                  58   ALL(b):[(t,b) e g => t e x & b e y]

                        U Spec, 49

 

                  59   (t,u) e g => t e x & u e y

                        U Spec, 58

 

                  60   t e x & u e y

                        Detach, 59, 57

 

                  61   ALL(c2):[(t,c2) e xy <=> t e x & c2 e y]

                        U Spec, 10

 

                  62   (t,u) e xy <=> t e x & u e y

                        U Spec, 61

 

                  63   [(t,u) e xy => t e x & u e y]

                 & [t e x & u e y => (t,u) e xy]

                        Iff-And, 62

 

             Sufficient: For (t,u) e xy

 

                  64   t e x & u e y => (t,u) e xy

                        Split, 63

 

                  65   (t,u) e xy

                        Detach, 64, 60

 

         As Required:

 

            66   ALL(a):ALL(b):[(a,b) e g => (a,b) e xy]

                  4 Conclusion, 57

 

            67   Set'(g) & ALL(a):ALL(b):[(a,b) e g => (a,b) e xy]

                  Join, 48, 66

 

            68   g e pxy

                  Detach, 56, 67

 

            69   g e pxy

             & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]]

                  Join, 68, 50

 

            70   g e graphs

                  Detach, 53, 69

 

    As Required:

 

      71   ALL(g):[Set'(g)

         & ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

         & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

         & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

         => [(a,b) e g & (a,c) e g => b=c]]]

         => g e graphs]

            4 Conclusion, 47

 

    Joining results...

 

      72   ALL(g):[[g e graphs

         => Set'(g)

         & ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

         & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

         & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

         => [(a,b) e g & (a,c) e g => b=c]]]] & [Set'(g)

         & ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

         & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

         & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

         => [(a,b) e g & (a,c) e g => b=c]]]

         => g e graphs]]

            Join, 46, 71

 

    As Required:

 

      73   ALL(g):[g e graphs

         <=> Set'(g)

         & ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

         & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

         & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

         => [(a,b) e g & (a,c) e g => b=c]]]]

            Iff-And, 72

 

        

         Prove: ALL(g):[g e graphs

                => EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y

                => [fun(a1)=b <=> (a1,b) e g]]]

        

         Suppose...

 

            74   g e graphs

                  Premise

 

         Apply definition of graphs

 

            75   g e graphs

             <=> Set'(g)

             & ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

             & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]]

                  U Spec, 73

 

            76   [g e graphs => Set'(g)

             & ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

             & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]]]

             & [Set'(g)

             & ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

             & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]] => g e graphs]

                  Iff-And, 75

 

            77   g e graphs => Set'(g)

             & ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

             & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]]

                  Split, 76

 

            78   Set'(g)

             & ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

             & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]]

                  Detach, 77, 74

 

            79   Set'(g)

                  Split, 78

 

            80   ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

                  Split, 78

 

            81   ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]

                  Split, 78

 

         Apply Function Axiom  (1 variable)

 

            82   ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)

             => [ALL(a1):ALL(b):[(a1,b) e gra => a1 e dom & b e cod]

             & ALL(a1):[a1 e dom => EXIST(b):[b e cod & (a1,b) e gra]]

             & ALL(a1):ALL(b1):ALL(b2):[a1 e dom & b1 e cod & b2 e cod

             => [(a1,b1) e gra & (a1,b2) e gra => b1=b2]]

             => EXIST(fun):ALL(a1):ALL(b):[a1 e dom & b e cod

             => [fun(a1)=b <=> (a1,b) e gra]]]]

                  Function

 

            83   ALL(cod):ALL(gra):[Set(x) & Set(cod) & Set'(gra)

             => [ALL(a1):ALL(b):[(a1,b) e gra => a1 e x & b e cod]

             & ALL(a1):[a1 e x => EXIST(b):[b e cod & (a1,b) e gra]]

             & ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e cod & b2 e cod

             => [(a1,b1) e gra & (a1,b2) e gra => b1=b2]]

             => EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e cod

             => [fun(a1)=b <=> (a1,b) e gra]]]]

                  U Spec, 82

 

            84   ALL(gra):[Set(x) & Set(y) & Set'(gra)

             => [ALL(a1):ALL(b):[(a1,b) e gra => a1 e x & b e y]

             & ALL(a1):[a1 e x => EXIST(b):[b e y & (a1,b) e gra]]

             & ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e y & b2 e y

             => [(a1,b1) e gra & (a1,b2) e gra => b1=b2]]

             => EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y

             => [fun(a1)=b <=> (a1,b) e gra]]]]

                  U Spec, 83

 

            85   ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

                  Split, 81

 

            86   ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]

                  Split, 81

 

            87   ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

             & ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

                  Join, 80, 85

 

            88   Set(x) & Set(y) & Set'(g)

             => [ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e y]

             & ALL(a1):[a1 e x => EXIST(b):[b e y & (a1,b) e g]]

             & ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e y & b2 e y

             => [(a1,b1) e g & (a1,b2) e g => b1=b2]]

             => EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y

             => [fun(a1)=b <=> (a1,b) e g]]]

                  U Spec, 84

 

            89   Set(x) & Set(y) & Set'(g)

                  Join, 1, 79

 

            90   ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e y]

             & ALL(a1):[a1 e x => EXIST(b):[b e y & (a1,b) e g]]

             & ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e y & b2 e y

             => [(a1,b1) e g & (a1,b2) e g => b1=b2]]

             => EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y

             => [fun(a1)=b <=> (a1,b) e g]]

                  Detach, 88, 89

 

            91   ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

             & ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

                  Join, 80, 85

 

            92   ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

             & ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

             & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

             => [(a,b) e g & (a,c) e g => b=c]]

                  Join, 91, 86

 

            93   EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y

             => [fun(a1)=b <=> (a1,b) e g]]

                  Detach, 90, 92

 

    As Required:

 

      94   ALL(g):[g e graphs

         => EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y

         => [fun(a1)=b <=> (a1,b) e g]]]

            4 Conclusion, 74

 

      95   Set(graphs)

         & ALL(g):[g e graphs

         <=> Set'(g)

         & ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

         & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

         & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

         => [(a,b) e g & (a,c) e g => b=c]]]]

            Join, 19, 73

 

      96   Set(graphs)

         & ALL(g):[g e graphs

         <=> Set'(g)

         & ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

         & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

         & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

         => [(a,b) e g & (a,c) e g => b=c]]]]

         & ALL(g):[g e graphs

         => EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y

         => [fun(a1)=b <=> (a1,b) e g]]]

            Join, 95, 94

 

As Required:

 

97   ALL(x):ALL(y):[Set(x) & Set(y)

    => EXIST(graphs):[Set(graphs)

    & ALL(g):[g e graphs

    <=> Set'(g)

    & ALL(a):ALL(b):[(a,b) e g => a e x & b e y]

    & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]

    & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

    => [(a,b) e g & (a,c) e g => b=c]]]]

    & ALL(g):[g e graphs

    => EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y

    => [fun(a1)=b <=> (a1,b) e g]]]]]

      4 Conclusion, 1