let f1, f2, f3 be Function of (2 -tuples_on BOOLEAN),BOOLEAN; :: thesis: 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; :: thesis: 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 ; :: thesis: {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} ; :: according to XBOOLE_0:def 10 :: thesis: {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 ; :: according to TARSKI:def 3 :: thesis: ( 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} ; :: thesis: 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; :: thesis: verum