let Y be non empty set ; :: thesis: for G being Subset of ()
for A, B, C, D, E, F being a_partition of Y
for z, u being Element of Y
for h being Function st G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & EqClass (z,(((C '/\' D) '/\' E) '/\' F)) = EqClass (u,(((C '/\' D) '/\' E) '/\' F)) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))

let G be Subset of (); :: thesis: for A, B, C, D, E, F being a_partition of Y
for z, u being Element of Y
for h being Function st G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & EqClass (z,(((C '/\' D) '/\' E) '/\' F)) = EqClass (u,(((C '/\' D) '/\' E) '/\' F)) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))

let A, B, C, D, E, F be a_partition of Y; :: thesis: for z, u being Element of Y
for h being Function st G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & EqClass (z,(((C '/\' D) '/\' E) '/\' F)) = EqClass (u,(((C '/\' D) '/\' E) '/\' F)) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))

let z, u be Element of Y; :: thesis: for h being Function st G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & EqClass (z,(((C '/\' D) '/\' E) '/\' F)) = EqClass (u,(((C '/\' D) '/\' E) '/\' F)) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))

let h be Function; :: thesis: ( G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & EqClass (z,(((C '/\' D) '/\' E) '/\' F)) = EqClass (u,(((C '/\' D) '/\' E) '/\' F)) implies EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G))) )
assume that
A1: G is independent and
A2: G = {A,B,C,D,E,F} and
A3: ( A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F ) and
A4: EqClass (z,(((C '/\' D) '/\' E) '/\' F)) = EqClass (u,(((C '/\' D) '/\' E) '/\' F)) ; :: thesis: EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))
set h = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)));
A5: ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . A = EqClass (z,A) by ;
set I = EqClass (z,A);
set GG = EqClass (u,((((B '/\' C) '/\' D) '/\' E) '/\' F));
set H = EqClass (z,(CompF (B,G)));
A6: A '/\' (((C '/\' D) '/\' E) '/\' F) = (A '/\' ((C '/\' D) '/\' E)) '/\' F by PARTIT1:14
.= ((A '/\' (C '/\' D)) '/\' E) '/\' F by PARTIT1:14
.= (((A '/\' C) '/\' D) '/\' E) '/\' F by PARTIT1:14 ;
EqClass (u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) = (EqClass (u,(((B '/\' C) '/\' D) '/\' E))) /\ (EqClass (u,F)) by Th1;
then EqClass (u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) = ((EqClass (u,((B '/\' C) '/\' D))) /\ (EqClass (u,E))) /\ (EqClass (u,F)) by Th1;
then EqClass (u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) = (((EqClass (u,(B '/\' C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F)) by Th1;
then A7: (EqClass (u,((((B '/\' C) '/\' D) '/\' E) '/\' F))) /\ (EqClass (z,A)) = (((((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (z,A)) by Th1;
A8: ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . B = EqClass (u,B) by ;
A9: ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . F = EqClass (u,F) by ;
A10: ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . E = EqClass (u,E) by ;
A11: ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . D = EqClass (u,D) by ;
A12: ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . C = EqClass (u,C) by ;
A13: rng ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) = {(((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . A),(((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . B),(((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . C),(((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . D),(((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . E),(((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . F)} by Th39;
rng ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) c= bool Y
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) or t in bool Y )
assume A14: t in rng ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) ; :: thesis: t in bool Y
now :: thesis: ( ( t = ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . A & t in bool Y ) or ( t = ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . B & t in bool Y ) or ( t = ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . C & t in bool Y ) or ( t = ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . D & t in bool Y ) or ( t = ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . E & t in bool Y ) or ( t = ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . F & t in bool Y ) )
per cases ( t = ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . A or t = ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . B or t = ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . C or t = ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . D or t = ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . E or t = ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . F ) by ;
case t = ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . A ; :: thesis: t in bool Y
hence t in bool Y by A5; :: thesis: verum
end;
case t = ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . B ; :: thesis: t in bool Y
hence t in bool Y by A8; :: thesis: verum
end;
case t = ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . C ; :: thesis: t in bool Y
hence t in bool Y by A12; :: thesis: verum
end;
case t = ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . D ; :: thesis: t in bool Y
hence t in bool Y by A11; :: thesis: verum
end;
case t = ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . E ; :: thesis: t in bool Y
hence t in bool Y by A10; :: thesis: verum
end;
case t = ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . F ; :: thesis: t in bool Y
hence t in bool Y by A9; :: thesis: verum
end;
end;
end;
hence t in bool Y ; :: thesis: verum
end;
then reconsider FF = rng ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) as Subset-Family of Y ;
A15: dom ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) = G by ;
then A in dom ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) by ;
then A16: ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . A in rng ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then A17: Intersect FF = meet (rng ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A))))) by SETFAM_1:def 9;
for d being set st d in G holds
((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d
proof
let d be set ; :: thesis: ( d in G implies ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d )
assume A18: d in G ; :: thesis: ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d
now :: thesis: ( ( d = A & ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d ) or ( d = B & ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d ) or ( d = C & ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d ) or ( d = D & ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d ) or ( d = E & ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d ) or ( d = F & ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d ) )
per cases ( d = A or d = B or d = C or d = D or d = E or d = F ) by ;
case d = A ; :: thesis: ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d
hence ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d by A5; :: thesis: verum
end;
case d = B ; :: thesis: ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d
hence ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d by A8; :: thesis: verum
end;
case d = C ; :: thesis: ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d
hence ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d by A12; :: thesis: verum
end;
case d = D ; :: thesis: ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d
hence ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d by A11; :: thesis: verum
end;
case d = E ; :: thesis: ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d
hence ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d by A10; :: thesis: verum
end;
case d = F ; :: thesis: ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d
hence ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d by A9; :: thesis: verum
end;
end;
end;
hence ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . d in d ; :: thesis: verum
end;
then Intersect FF <> {} by ;
then consider m being object such that
A19: m in Intersect FF by XBOOLE_0:def 1;
D in dom ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) by ;
then ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . D in rng ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . D by ;
then A20: m in EqClass (u,D) by ;
C in dom ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) by ;
then ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . C in rng ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . C by ;
then A21: m in EqClass (u,C) by ;
B in dom ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) by ;
then ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . B in rng ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . B by ;
then m in EqClass (u,B) by ;
then m in (EqClass (u,B)) /\ (EqClass (u,C)) by ;
then A22: m in ((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D)) by ;
F in dom ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) by ;
then ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . F in rng ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . F by ;
then A23: m in EqClass (u,F) by ;
E in dom ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) by ;
then ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . E in rng ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . E by ;
then m in EqClass (u,E) by ;
then m in (((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E)) by ;
then A24: m in ((((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F)) by ;
m in ((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (A .--> (EqClass (z,A)))) . A by ;
then m in EqClass (z,A) by ;
then (EqClass (u,((((B '/\' C) '/\' D) '/\' E) '/\' F))) /\ (EqClass (z,A)) <> {} by ;
then consider p being object such that
A25: p in (EqClass (u,((((B '/\' C) '/\' D) '/\' E) '/\' F))) /\ (EqClass (z,A)) by XBOOLE_0:def 1;
reconsider p = p as Element of Y by A25;
A26: p in EqClass (u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) by ;
set L = EqClass (z,(((C '/\' D) '/\' E) '/\' F));
EqClass (u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) = EqClass (u,(((B '/\' (C '/\' D)) '/\' E) '/\' F)) by PARTIT1:14;
then EqClass (u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) = EqClass (u,((B '/\' ((C '/\' D) '/\' E)) '/\' F)) by PARTIT1:14;
then EqClass (u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) = EqClass (u,(B '/\' (((C '/\' D) '/\' E) '/\' F))) by PARTIT1:14;
then A27: EqClass (u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) c= EqClass (z,(((C '/\' D) '/\' E) '/\' F)) by ;
A28: z in EqClass (z,(CompF (B,G))) by EQREL_1:def 6;
set K = EqClass (p,(((C '/\' D) '/\' E) '/\' F));
( p in EqClass (p,(((C '/\' D) '/\' E) '/\' F)) & p in EqClass (z,A) ) by ;
then A29: p in (EqClass (z,A)) /\ (EqClass (p,(((C '/\' D) '/\' E) '/\' F))) by XBOOLE_0:def 4;
then ( (EqClass (z,A)) /\ (EqClass (p,(((C '/\' D) '/\' E) '/\' F))) in INTERSECTION (A,(((C '/\' D) '/\' E) '/\' F)) & not (EqClass (z,A)) /\ (EqClass (p,(((C '/\' D) '/\' E) '/\' F))) in ) by ;
then (EqClass (z,A)) /\ (EqClass (p,(((C '/\' D) '/\' E) '/\' F))) in (INTERSECTION (A,(((C '/\' D) '/\' E) '/\' F))) \ by XBOOLE_0:def 5;
then A30: (EqClass (z,A)) /\ (EqClass (p,(((C '/\' D) '/\' E) '/\' F))) in A '/\' (((C '/\' D) '/\' E) '/\' F) by PARTIT1:def 4;
p in EqClass (p,(((C '/\' D) '/\' E) '/\' F)) by EQREL_1:def 6;
then EqClass (p,(((C '/\' D) '/\' E) '/\' F)) meets EqClass (z,(((C '/\' D) '/\' E) '/\' F)) by ;
then EqClass (p,(((C '/\' D) '/\' E) '/\' F)) = EqClass (z,(((C '/\' D) '/\' E) '/\' F)) by EQREL_1:41;
then A31: z in EqClass (p,(((C '/\' D) '/\' E) '/\' F)) by EQREL_1:def 6;
z in EqClass (z,A) by EQREL_1:def 6;
then A32: z in (EqClass (z,A)) /\ (EqClass (p,(((C '/\' D) '/\' E) '/\' F))) by ;
CompF (B,G) = (((A '/\' C) '/\' D) '/\' E) '/\' F by A2, A3, Th32;
then A33: ( (EqClass (z,A)) /\ (EqClass (p,(((C '/\' D) '/\' E) '/\' F))) = EqClass (z,(CompF (B,G))) or (EqClass (z,A)) /\ (EqClass (p,(((C '/\' D) '/\' E) '/\' F))) misses EqClass (z,(CompF (B,G))) ) by ;
EqClass (u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) = EqClass (u,(CompF (A,G))) by A2, A3, Th31;
hence EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G))) by ; :: thesis: verum