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

let A, B, C, D, E, F, J 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} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J & EqClass (z,((((C '/\' D) '/\' E) '/\' F) '/\' J)) = EqClass (u,((((C '/\' D) '/\' E) '/\' F) '/\' J)) 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} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J & EqClass (z,((((C '/\' D) '/\' E) '/\' F) '/\' J)) = EqClass (u,((((C '/\' D) '/\' E) '/\' F) '/\' J)) 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} and
A3: ( A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J ) and
A4: EqClass (z,((((C '/\' D) '/\' E) '/\' F) '/\' J)) = EqClass (u,((((C '/\' D) '/\' E) '/\' F) '/\' J)) ; :: 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)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (A .--> (EqClass (z,A)))) . A = EqClass (z,A) by ;
reconsider L = EqClass (z,((((C '/\' D) '/\' E) '/\' F) '/\' J)) as set ;
reconsider GG = EqClass (u,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J)) as set ;
reconsider I = EqClass (z,A) as set ;
GG = (EqClass (u,((((B '/\' C) '/\' D) '/\' E) '/\' F))) /\ (EqClass (u,J)) by Th1;
then GG = ((EqClass (u,(((B '/\' C) '/\' D) '/\' E))) /\ (EqClass (u,F))) /\ (EqClass (u,J)) by Th1;
then GG = (((EqClass (u,((B '/\' C) '/\' D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (u,J)) by Th1;
then GG = ((((EqClass (u,(B '/\' C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (u,J)) by Th1;
then A6: GG /\ I = ((((((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (u,J))) /\ (EqClass (z,A)) by Th1;
A7: CompF (A,G) = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J by A2, A3, Th42;
reconsider HH = EqClass (z,(CompF (B,G))) as set ;
A8: z in HH by EQREL_1:def 6;
A9: A '/\' ((((C '/\' D) '/\' E) '/\' F) '/\' J) = (A '/\' (((C '/\' D) '/\' E) '/\' F)) '/\' J by PARTIT1:14
.= ((A '/\' ((C '/\' D) '/\' E)) '/\' F) '/\' J by PARTIT1:14
.= (((A '/\' (C '/\' D)) '/\' E) '/\' F) '/\' J by PARTIT1:14
.= ((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J by PARTIT1:14 ;
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)))) +* (A .--> (EqClass (z,A)))) . B = EqClass (u,B) by ;
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)))) +* (A .--> (EqClass (z,A)))) . F = EqClass (u,F) by ;
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)))) +* (A .--> (EqClass (z,A)))) . E = EqClass (u,E) by ;
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)))) +* (A .--> (EqClass (z,A)))) . J = EqClass (u,J) by ;
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)))) +* (A .--> (EqClass (z,A)))) . D = EqClass (u,D) by ;
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)))) +* (A .--> (EqClass (z,A)))) . C = EqClass (u,C) by ;
A16: 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)))) +* (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)))) +* (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)))) +* (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)))) +* (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)))) +* (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)))) +* (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)))) +* (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)))) +* (A .--> (EqClass (z,A)))) . J)} by Th51;
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)))) +* (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)))) +* (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)))) +* (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)))) +* (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)))) +* (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)))) +* (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)))) +* (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)))) +* (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)))) +* (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)))) +* (A .--> (EqClass (z,A)))) . J ) by ;
hence t in bool Y by A5, A10, A15, A14, A12, A11, A13; :: 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)))) +* (A .--> (EqClass (z,A)))) as Subset-Family of Y ;
A17: 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)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (A .--> (EqClass (z,A)))) by ;
then A18: (((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (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)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then A19: 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)))) +* (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)))) +* (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)))) +* (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)))) +* (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 ) by ;
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)))) +* (A .--> (EqClass (z,A)))) . d in d by A5, A10, A15, A14, A12, A11, A13; :: thesis: verum
end;
then Intersect FF <> {} by ;
then consider m being object such that
A20: 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)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (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)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
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)))) +* (J .--> (EqClass (u,J)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (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)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in EqClass (u,B) by ;
then A22: m in (EqClass (u,B)) /\ (EqClass (u,C)) by ;
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)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (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)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in EqClass (u,D) by ;
then A23: m in ((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D)) by ;
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)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (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)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in EqClass (u,E) by ;
then A24: m in (((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E)) by ;
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)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (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)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in EqClass (u,F) by ;
then A25: m in ((((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F)) by ;
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)))) +* (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)))) +* (J .--> (EqClass (u,J)))) +* (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)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in EqClass (u,J) by ;
then A26: m in (((((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (u,J)) by ;
m in EqClass (z,A) by ;
then A27: GG /\ I <> {} by ;
then consider p being object such that
A28: p in GG /\ I by XBOOLE_0:def 1;
( GG /\ I in INTERSECTION (A,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J)) & not GG /\ I in ) by ;
then GG /\ I in (INTERSECTION (A,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J))) \ by XBOOLE_0:def 5;
then GG /\ I in A '/\' (((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) by PARTIT1:def 4;
then reconsider p = p as Element of Y by A28;
A29: p in GG by ;
reconsider K = EqClass (p,((((C '/\' D) '/\' E) '/\' F) '/\' J)) as set ;
A30: p in EqClass (p,((((C '/\' D) '/\' E) '/\' F) '/\' J)) by EQREL_1:def 6;
GG = EqClass (u,((((B '/\' (C '/\' D)) '/\' E) '/\' F) '/\' J)) by PARTIT1:14;
then GG = EqClass (u,(((B '/\' ((C '/\' D) '/\' E)) '/\' F) '/\' J)) by PARTIT1:14;
then GG = EqClass (u,((B '/\' (((C '/\' D) '/\' E) '/\' F)) '/\' J)) by PARTIT1:14;
then GG = EqClass (u,(B '/\' ((((C '/\' D) '/\' E) '/\' F) '/\' J))) by PARTIT1:14;
then GG c= L by ;
then K meets L by ;
then K = L by EQREL_1:41;
then A31: z in K by EQREL_1:def 6;
( p in K & p in I ) by ;
then A32: p in I /\ K by XBOOLE_0:def 4;
then ( I /\ K in INTERSECTION (A,((((C '/\' D) '/\' E) '/\' F) '/\' J)) & not I /\ K in ) by ;
then I /\ K in (INTERSECTION (A,((((C '/\' D) '/\' E) '/\' F) '/\' J))) \ by XBOOLE_0:def 5;
then A33: I /\ K in A '/\' ((((C '/\' D) '/\' E) '/\' F) '/\' J) by PARTIT1:def 4;
z in I by EQREL_1:def 6;
then z in I /\ K by ;
then A34: I /\ K meets HH by ;
CompF (B,G) = ((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J by A2, A3, Th43;
then p in HH by ;
hence EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G))) by ; :: thesis: verum