let f1, f2, f3 be Function of (2 -tuples_on BOOLEAN),BOOLEAN; :: thesis: for x, y, z being set st x <> [<*y,z*>,f2] & y <> [<*z,x*>,f3] & z <> [<*x,y*>,f1] holds
( not [<*x,y*>,f1] in {y,z} & not z in {[<*x,y*>,f1],[<*y,z*>,f2]} & not x in {[<*x,y*>,f1],[<*y,z*>,f2]} & not [<*z,x*>,f3] in {x,y,z} )
let x, y, z be set ; :: thesis: ( x <> [<*y,z*>,f2] & y <> [<*z,x*>,f3] & z <> [<*x,y*>,f1] implies ( not [<*x,y*>,f1] in {y,z} & not z in {[<*x,y*>,f1],[<*y,z*>,f2]} & not x in {[<*x,y*>,f1],[<*y,z*>,f2]} & not [<*z,x*>,f3] in {x,y,z} ) )
set xy = {{<*x,y*>},{<*x,y*>,f1}};
set yz = {{<*y,z*>},{<*y,z*>,f2}};
set zx = {{<*z,x*>},{<*z,x*>,f3}};
assume that
A1: x <> [<*y,z*>,f2] and
A2: y <> [<*z,x*>,f3] and
A3: z <> [<*x,y*>,f1] ; :: thesis: ( not [<*x,y*>,f1] in {y,z} & not z in {[<*x,y*>,f1],[<*y,z*>,f2]} & not x in {[<*x,y*>,f1],[<*y,z*>,f2]} & not [<*z,x*>,f3] in {x,y,z} )
A4: ( <*x,y*> in {<*x,y*>} & {<*x,y*>} in {{<*x,y*>},{<*x,y*>,f1}} ) by TARSKI:def 1, TARSKI:def 2;
dom <*x,y*> = Seg 2 by FINSEQ_1:89;
then A5: 2 in dom <*x,y*> by FINSEQ_1:1;
<*x,y*> . 2 = y by FINSEQ_1:44;
then A6: [2,y] in <*x,y*> by A5, FUNCT_1:1;
( y in {2,y} & {2,y} in {{2},{2,y}} ) by TARSKI:def 2;
then y <> {{<*x,y*>},{<*x,y*>,f1}} by A6, A4, XREGULAR:9;
hence not [<*x,y*>,f1] in {y,z} by A3, TARSKI:def 2; :: thesis: ( not z in {[<*x,y*>,f1],[<*y,z*>,f2]} & not x in {[<*x,y*>,f1],[<*y,z*>,f2]} & not [<*z,x*>,f3] in {x,y,z} )
A7: ( z in {2,z} & {2,z} in {{2},{2,z}} ) by TARSKI:def 2;
A8: ( <*x,y*> in {<*x,y*>} & {<*x,y*>} in {{<*x,y*>},{<*x,y*>,f1}} ) by TARSKI:def 1, TARSKI:def 2;
<*z*> = {[1,z]} by FINSEQ_1:def 5;
then A9: [1,z] in <*z*> by TARSKI:def 1;
<*x*> = {[1,x]} by FINSEQ_1:def 5;
then A10: [1,x] in <*x*> by TARSKI:def 1;
dom <*z,x*> = Seg 2 by FINSEQ_1:89;
then A11: 2 in dom <*z,x*> by FINSEQ_1:1;
<*z,x*> . 2 = x by FINSEQ_1:44;
then A12: [2,x] in <*z,x*> by A11, FUNCT_1:1;
<*z,x*> = <*z*> ^ <*x*> by FINSEQ_1:def 9;
then A13: <*z*> c= <*z,x*> by FINSEQ_6:10;
dom <*y,z*> = Seg 2 by FINSEQ_1:89;
then A14: 2 in dom <*y,z*> by FINSEQ_1:1;
<*y,z*> . 2 = z by FINSEQ_1:44;
then A15: [2,z] in <*y,z*> by A14, FUNCT_1:1;
<*x,y*> = <*x*> ^ <*y*> by FINSEQ_1:def 9;
then A16: <*x*> c= <*x,y*> by FINSEQ_6:10;
( <*y,z*> in {<*y,z*>} & {<*y,z*>} in {{<*y,z*>},{<*y,z*>,f2}} ) by TARSKI:def 1, TARSKI:def 2;
then A17: z <> {{<*y,z*>},{<*y,z*>,f2}} by A7, A15, XREGULAR:9;
( x in {1,x} & {1,x} in {{1},{1,x}} ) by TARSKI:def 2;
then x <> {{<*x,y*>},{<*x,y*>,f1}} by A16, A10, A8, XREGULAR:9;
hence ( not z in {[<*x,y*>,f1],[<*y,z*>,f2]} & not x in {[<*x,y*>,f1],[<*y,z*>,f2]} ) by A1, A3, A17, TARSKI:def 2; :: thesis: not [<*z,x*>,f3] in {x,y,z}
A18: ( <*z,x*> in {<*z,x*>} & {<*z,x*>} in {{<*z,x*>},{<*z,x*>,f3}} ) by TARSKI:def 1, TARSKI:def 2;
A19: ( <*z,x*> in {<*z,x*>} & {<*z,x*>} in {{<*z,x*>},{<*z,x*>,f3}} ) by TARSKI:def 1, TARSKI:def 2;
( x in {2,x} & {2,x} in {{2},{2,x}} ) by TARSKI:def 2;
then A20: x <> {{<*z,x*>},{<*z,x*>,f3}} by A12, A18, XREGULAR:9;
( z in {1,z} & {1,z} in {{1},{1,z}} ) by TARSKI:def 2;
then z <> {{<*z,x*>},{<*z,x*>,f3}} by A13, A9, A19, XREGULAR:9;
hence not [<*z,x*>,f3] in {x,y,z} by A2, A20, ENUMSET1:def 1; :: thesis: verum