let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M & EqClass (z,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) = EqClass (u,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))
let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C, D, E, F, J, M being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M & EqClass (z,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) = EqClass (u,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))
let A, B, C, D, E, F, J, M be a_partition of Y; :: thesis: for z, u being Element of Y st G is independent & G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M & EqClass (z,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) = EqClass (u,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))
let z, u be Element of Y; :: thesis: ( G is independent & G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M & EqClass (z,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) = EqClass (u,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) 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,J,M} and
A3: ( A <> B & A <> C & A <> D & A <> E & A <> F & A <> J ) and
A4: A <> M and
A5: ( B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M ) and
A6: EqClass (z,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) = EqClass (u,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) ; :: 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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)));
A7: ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . B = EqClass (u,B) by A3, A5, Th62;
set HH = EqClass (z,(CompF (B,G)));
set I = EqClass (z,A);
set GG = EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M));
A8: EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) = EqClass (u,(CompF (A,G))) by A2, A3, A4, A5, Th54;
EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) = (EqClass (u,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J))) /\ (EqClass (u,M)) by Th1;
then EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) = ((EqClass (u,((((B '/\' C) '/\' D) '/\' E) '/\' F))) /\ (EqClass (u,J))) /\ (EqClass (u,M)) by Th1;
then EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) = (((EqClass (u,(((B '/\' C) '/\' D) '/\' E))) /\ (EqClass (u,F))) /\ (EqClass (u,J))) /\ (EqClass (u,M)) by Th1;
then EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) = ((((EqClass (u,((B '/\' C) '/\' D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (u,J))) /\ (EqClass (u,M)) by Th1;
then EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) = (((((EqClass (u,(B '/\' C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (u,J))) /\ (EqClass (u,M)) by Th1;
then A9: (EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M))) /\ (EqClass (z,A)) = (((((((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (u,J))) /\ (EqClass (u,M))) /\ (EqClass (z,A)) by Th1;
A10: ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . A = EqClass (z,A) by FUNCT_7:94;
A11: ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . C = EqClass (u,C) by A3, A5, Th62;
A12: ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . M = EqClass (u,M) by A4, Lm1;
A13: ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . J = EqClass (u,J) by A3, A5, Th62;
A14: ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . F = EqClass (u,F) by A3, A5, Th62;
A15: ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . E = EqClass (u,E) by A3, A5, Th62;
A16: ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . D = EqClass (u,D) by A3, A5, Th62;
A17: rng ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) = {(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . F),(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . J),(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . M)} by Th64;
rng ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) or t in bool Y )
assume t in rng ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) ; :: thesis: t in bool Y
then ( t = ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . F or t = ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . J or t = ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . M ) by A17, ENUMSET1:def 6;
hence t in bool Y by A10, A7, A11, A16, A15, A14, A13, A12; :: 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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) as Subset-Family of Y ;
A18: dom ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) = G by A2, Th63;
then A in dom ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) by A2, ENUMSET1:def 6;
then A19: ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then A20: Intersect FF = meet (rng ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . d in d )
assume d in G ; :: thesis: ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . d in d
then ( d = A or d = B or d = C or d = D or d = E or d = F or d = J or d = M ) by A2, ENUMSET1:def 6;
hence ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . d in d by A10, A7, A11, A16, A15, A14, A13, A12; :: thesis: verum

end;

then Intersect FF <> {} by A1, A18, BVFUNC_2:def 5;
then consider m being object such that
A21: m in Intersect FF by XBOOLE_0:def 1;
C in dom ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) by A2, A18, ENUMSET1:def 6;
then ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then A22: m in EqClass (u,C) by A11, A20, A21, SETFAM_1:def 1;
B in dom ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) by A2, A18, ENUMSET1:def 6;
then ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in EqClass (u,B) by A7, A20, A21, SETFAM_1:def 1;
then A23: m in (EqClass (u,B)) /\ (EqClass (u,C)) by A22, XBOOLE_0:def 4;
D in dom ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) by A2, A18, ENUMSET1:def 6;
then ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in EqClass (u,D) by A16, A20, A21, SETFAM_1:def 1;
then A24: m in ((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D)) by A23, XBOOLE_0:def 4;
E in dom ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) by A2, A18, ENUMSET1:def 6;
then ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in EqClass (u,E) by A15, A20, A21, SETFAM_1:def 1;
then A25: m in (((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E)) by A24, XBOOLE_0:def 4;
F in dom ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) by A2, A18, ENUMSET1:def 6;
then ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in EqClass (u,F) by A14, A20, A21, SETFAM_1:def 1;
then A26: m in ((((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F)) by A25, XBOOLE_0:def 4;
J in dom ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) by A2, A18, ENUMSET1:def 6;
then ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . J in rng ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in EqClass (u,J) by A13, A20, A21, SETFAM_1:def 1;
then A27: m in (((((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (u,J)) by A26, XBOOLE_0:def 4;
M in dom ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) by A2, A18, ENUMSET1:def 6;
then ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . M in rng ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in EqClass (u,M) by A12, A20, A21, SETFAM_1:def 1;
then A28: m in ((((((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (u,J))) /\ (EqClass (u,M)) by A27, XBOOLE_0:def 4;
m in EqClass (z,A) by A10, A19, A20, A21, SETFAM_1:def 1;
then (EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M))) /\ (EqClass (z,A)) <> {} by A9, A28, XBOOLE_0:def 4;
then consider p being object such that
A29: p in (EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M))) /\ (EqClass (z,A)) by XBOOLE_0:def 1;
reconsider p = p as Element of Y by A29;
reconsider K = EqClass (p,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) as set ;
A30: p in EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) by A29, XBOOLE_0:def 4;
reconsider L = EqClass (z,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) as set ;
A31: p in EqClass (p,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) by EQREL_1:def 6;
EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) = EqClass (u,(((((B '/\' (C '/\' D)) '/\' E) '/\' F) '/\' J) '/\' M)) by PARTIT1:14;
then EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) = EqClass (u,((((B '/\' ((C '/\' D) '/\' E)) '/\' F) '/\' J) '/\' M)) by PARTIT1:14;
then EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) = EqClass (u,(((B '/\' (((C '/\' D) '/\' E) '/\' F)) '/\' J) '/\' M)) by PARTIT1:14;
then EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) = EqClass (u,((B '/\' ((((C '/\' D) '/\' E) '/\' F) '/\' J)) '/\' M)) by PARTIT1:14;
then EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) = EqClass (u,(B '/\' (((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M))) by PARTIT1:14;
then EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) c= L by A6, BVFUNC11:3;
then K meets L by A30, A31, XBOOLE_0:3;
then K = L by EQREL_1:41;
then A32: z in K by EQREL_1:def 6;
A33: z in EqClass (z,(CompF (B,G))) by EQREL_1:def 6;
z in EqClass (z,A) by EQREL_1:def 6;
then z in (EqClass (z,A)) /\ K by A32, XBOOLE_0:def 4;
then A34: (EqClass (z,A)) /\ K meets EqClass (z,(CompF (B,G))) by A33, XBOOLE_0:3;
A35: A '/\' (((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = (A '/\' ((((C '/\' D) '/\' E) '/\' F) '/\' J)) '/\' M by PARTIT1:14
.= ((A '/\' (((C '/\' D) '/\' E) '/\' F)) '/\' J) '/\' M by PARTIT1:14
.= (((A '/\' ((C '/\' D) '/\' E)) '/\' F) '/\' J) '/\' M by PARTIT1:14
.= ((((A '/\' (C '/\' D)) '/\' E) '/\' F) '/\' J) '/\' M by PARTIT1:14
.= (((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M by PARTIT1:14 ;
( p in K & p in EqClass (z,A) ) by A29, EQREL_1:def 6, XBOOLE_0:def 4;
then A36: p in (EqClass (z,A)) /\ K by XBOOLE_0:def 4;
then ( (EqClass (z,A)) /\ K in INTERSECTION (A,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) & not (EqClass (z,A)) /\ K in {{}} ) by SETFAM_1:def 5, TARSKI:def 1;
then (EqClass (z,A)) /\ K in (INTERSECTION (A,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M))) \ {{}} by XBOOLE_0:def 5;
then A37: (EqClass (z,A)) /\ K in A '/\' (((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) by PARTIT1:def 4;
CompF (B,G) = (((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M by A2, A3, A4, A5, Th55;
then p in EqClass (z,(CompF (B,G))) by A36, A37, A34, A35, EQREL_1:def 4;
hence EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G))) by A8, A30, XBOOLE_0:3; :: thesis: verum