let f1, f2, f3 be Function of (2 -tuples_on BOOLEAN),BOOLEAN; for f4 being Function of (3 -tuples_on BOOLEAN),BOOLEAN
for x, y, z being set holds {x,y,z} \ {[<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f4]} = {x,y,z}
let f4 be Function of (3 -tuples_on BOOLEAN),BOOLEAN; for x, y, z being set holds {x,y,z} \ {[<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f4]} = {x,y,z}
let x, y, z be set ; {x,y,z} \ {[<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f4]} = {x,y,z}
set xy = [<*x,y*>,f1];
set yz = [<*y,z*>,f2];
set zx = [<*z,x*>,f3];
set xyz = [<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f4];
A1:
<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*> . 3 = [<*z,x*>,f3]
by FINSEQ_1:45;
len <*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*> = 3
by FINSEQ_1:45;
then A2:
Seg 3 = dom <*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>
by FINSEQ_1:def 3;
then
3 in dom <*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>
by FINSEQ_1:1;
then
[3,[<*z,x*>,f3]] in <*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>
by A1, FUNCT_1:1;
then
[<*z,x*>,f3] in rng <*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>
by XTUPLE_0:def 13;
then A3:
the_rank_of [<*z,x*>,f3] in the_rank_of [<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f4]
by CLASSES1:82;
rng <*y,z*> = {y,z}
by FINSEQ_2:127;
then A4:
z in rng <*y,z*>
by TARSKI:def 2;
thus
{x,y,z} \ {[<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f4]} c= {x,y,z}
; XBOOLE_0:def 10 {x,y,z} c= {x,y,z} \ {[<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f4]}
A5:
<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*> . 2 = [<*y,z*>,f2]
by FINSEQ_1:45;
let a be object ; TARSKI:def 3 ( not a in {x,y,z} or a in {x,y,z} \ {[<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f4]} )
A6:
<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*> . 1 = [<*x,y*>,f1]
by FINSEQ_1:45;
1 in dom <*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>
by A2, FINSEQ_1:1;
then
[1,[<*x,y*>,f1]] in <*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>
by A6, FUNCT_1:1;
then
[<*x,y*>,f1] in rng <*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>
by XTUPLE_0:def 13;
then A7:
the_rank_of [<*x,y*>,f1] in the_rank_of [<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f4]
by CLASSES1:82;
rng <*z,x*> = {z,x}
by FINSEQ_2:127;
then A8:
x in rng <*z,x*>
by TARSKI:def 2;
2 in dom <*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>
by A2, FINSEQ_1:1;
then
[2,[<*y,z*>,f2]] in <*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>
by A5, FUNCT_1:1;
then
[<*y,z*>,f2] in rng <*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>
by XTUPLE_0:def 13;
then A9:
the_rank_of [<*y,z*>,f2] in the_rank_of [<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f4]
by CLASSES1:82;
rng <*x,y*> = {x,y}
by FINSEQ_2:127;
then A10:
y in rng <*x,y*>
by TARSKI:def 2;
assume A11:
a in {x,y,z}
; a in {x,y,z} \ {[<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f4]}
then
( a = x or a = y or a = z )
by ENUMSET1:def 1;
then
a <> [<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f4]
by A8, A3, A10, A7, A4, A9, CLASSES1:82;
then
not a in {[<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f4]}
by TARSKI:def 1;
hence
a in {x,y,z} \ {[<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f4]}
by A11, XBOOLE_0:def 5; verum