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*>,f1];
set yz = [<*y,z*>,f2];
set zx = [<*z,x*>,f3];
assume A1: ( x <> [<*y,z*>,f2] & y <> [<*z,x*>,f3] & 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} )
A2: ( y in {1,y} & y in {2,y} ) by TARSKI:def 2;
A3: ( {1,y} in [1,y] & {2,y} in [2,y] ) by TARSKI:def 2;
A4: ( <*y,z*> in {<*y,z*>} & {<*y,z*>} in [<*y,z*>,f2] ) by TARSKI:def 1, TARSKI:def 2;
A5: z in {2,z} by TARSKI:def 2;
A6: {2,z} in [2,z] by TARSKI:def 2;
( 2 in dom <*y,z*> & <*y,z*> . 2 = z )

proof

dom <*y,z*> = Seg 2 by FINSEQ_3:29;
hence ( 2 in dom <*y,z*> & <*y,z*> . 2 = z ) by FINSEQ_1:3, FINSEQ_1:61; :: thesis: verum

end;

then [2,z] in <*y,z*> by FUNCT_1:8;
then A7: z <> [<*y,z*>,f2] by A4, A5, A6, ORDINAL1:5;
( 2 in dom <*x,y*> & <*x,y*> . 2 = y )

proof

dom <*x,y*> = Seg 2 by FINSEQ_3:29;
hence ( 2 in dom <*x,y*> & <*x,y*> . 2 = y ) by FINSEQ_1:3, FINSEQ_1:61; :: thesis: verum

end;

then A8: [2,y] in <*x,y*> by FUNCT_1:8;
( <*x,y*> in {<*x,y*>} & {<*x,y*>} in [<*x,y*>,f1] ) by TARSKI:def 1, TARSKI:def 2;
then y <> [<*x,y*>,f1] by A2, A3, A8, ORDINAL1:5;
hence not [<*x,y*>,f1] in {y,z} by A1, 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} )
A9: x in {1,x} by TARSKI:def 2;
A10: {1,x} in [1,x] by TARSKI:def 2;
<*x,y*> = <*x*> ^ <*y*> by FINSEQ_1:def 9;
then A11: <*x*> c= <*x,y*> by FINSEQ_6:12;
<*x*> = {[1,x]} by FINSEQ_1:def 5;
then A12: [1,x] in <*x*> by TARSKI:def 1;
( <*x,y*> in {<*x,y*>} & {<*x,y*>} in [<*x,y*>,f1] ) by TARSKI:def 1, TARSKI:def 2;
then x <> [<*x,y*>,f1] by A9, A10, A11, A12, ORDINAL1:5;
hence ( not z in {[<*x,y*>,f1],[<*y,z*>,f2]} & not x in {[<*x,y*>,f1],[<*y,z*>,f2]} ) by A1, A7, TARSKI:def 2; :: thesis: not [<*z,x*>,f3] in {x,y,z}
A13: x in {2,x} by TARSKI:def 2;
A14: {2,x} in [2,x] by TARSKI:def 2;
( 2 in dom <*z,x*> & <*z,x*> . 2 = x )

proof

dom <*z,x*> = Seg 2 by FINSEQ_3:29;
hence ( 2 in dom <*z,x*> & <*z,x*> . 2 = x ) by FINSEQ_1:3, FINSEQ_1:61; :: thesis: verum

end;

then A15: [2,x] in <*z,x*> by FUNCT_1:8;
( <*z,x*> in {<*z,x*>} & {<*z,x*>} in [<*z,x*>,f3] ) by TARSKI:def 1, TARSKI:def 2;
then A16: x <> [<*z,x*>,f3] by A13, A14, A15, ORDINAL1:5;
A17: z in {1,z} by TARSKI:def 2;
A18: {1,z} in [1,z] by TARSKI:def 2;
<*z,x*> = <*z*> ^ <*x*> by FINSEQ_1:def 9;
then A19: <*z*> c= <*z,x*> by FINSEQ_6:12;
<*z*> = {[1,z]} by FINSEQ_1:def 5;
then A20: [1,z] in <*z*> by TARSKI:def 1;
( <*z,x*> in {<*z,x*>} & {<*z,x*>} in [<*z,x*>,f3] ) by TARSKI:def 1, TARSKI:def 2;
then z <> [<*z,x*>,f3] by A17, A18, A19, A20, ORDINAL1:5;
hence not [<*z,x*>,f3] in {x,y,z} by A1, A16, ENUMSET1:def 1; :: thesis: verum