let f1, f2, f3 be Function of (2 -tuples_on BOOLEAN),BOOLEAN; 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 ; ( 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 that
A1:
x <> [<*y,z*>,f2]
and
A2:
y <> [<*z,x*>,f3]
and
A3:
z <> [<*x,y*>,f1]
; ( 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*>,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,y] )
by TARSKI:def 2;
then
y <> [<*x,y*>,f1]
by A6, A4, ORDINAL1:3;
hence
not [<*x,y*>,f1] in {y,z}
by A3, TARSKI:def 2; ( 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,z] )
by TARSKI:def 2;
A8:
( <*x,y*> in {<*x,y*>} & {<*x,y*>} in [<*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*>,f2] )
by TARSKI:def 1, TARSKI:def 2;
then A17:
z <> [<*y,z*>,f2]
by A7, A15, ORDINAL1:3;
( x in {1,x} & {1,x} in [1,x] )
by TARSKI:def 2;
then
x <> [<*x,y*>,f1]
by A16, A10, A8, ORDINAL1:3;
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; not [<*z,x*>,f3] in {x,y,z}
A18:
( <*z,x*> in {<*z,x*>} & {<*z,x*>} in [<*z,x*>,f3] )
by TARSKI:def 1, TARSKI:def 2;
A19:
( <*z,x*> in {<*z,x*>} & {<*z,x*>} in [<*z,x*>,f3] )
by TARSKI:def 1, TARSKI:def 2;
( x in {2,x} & {2,x} in [2,x] )
by TARSKI:def 2;
then A20:
x <> [<*z,x*>,f3]
by A12, A18, ORDINAL1:3;
( z in {1,z} & {1,z} in [1,z] )
by TARSKI:def 2;
then
z <> [<*z,x*>,f3]
by A13, A9, A19, ORDINAL1:3;
hence
not [<*z,x*>,f3] in {x,y,z}
by A2, A20, ENUMSET1:def 1; verum