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

let G be Subset of (); :: 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 holds
(EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M))) /\ (EqClass (z,A)) <> {}

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 holds
(EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M))) /\ (EqClass (z,A)) <> {}

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 implies (EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M))) /\ (EqClass (z,A)) <> {} )
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 ) ; :: thesis: (EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M))) /\ (EqClass (z,A)) <> {}
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)));
A6: ((((((((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;
reconsider GG = EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) as set ;
reconsider I = EqClass (z,A) as set ;
GG = (EqClass (u,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J))) /\ (EqClass (u,M)) by Th1;
then GG = ((EqClass (u,((((B '/\' C) '/\' D) '/\' E) '/\' F))) /\ (EqClass (u,J))) /\ (EqClass (u,M)) by Th1;
then GG = (((EqClass (u,(((B '/\' C) '/\' D) '/\' E))) /\ (EqClass (u,F))) /\ (EqClass (u,J))) /\ (EqClass (u,M)) by Th1;
then GG = ((((EqClass (u,((B '/\' C) '/\' D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (u,J))) /\ (EqClass (u,M)) by Th1;
then GG = (((((EqClass (u,(B '/\' C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (u,J))) /\ (EqClass (u,M)) by Th1;
then A7: GG /\ I = (((((((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;
A8: ((((((((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;
A9: ((((((((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;
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)))) . M = EqClass (u,M) 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)))) +* (M .--> (EqClass (u,M)))) +* (A .--> (EqClass (z,A)))) . J = EqClass (u,J) 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)))) . F = EqClass (u,F) by A3, A5, Th62;
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)))) . E = EqClass (u,E) 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)))) . D = EqClass (u,D) by A3, A5, Th62;
A15: 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 ;
hence t in bool Y by A8, A6, A9, A14, A13, A12, A11, A10; :: 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 ;
A16: 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 ;
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 ;
then A17: ((((((((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 A18: 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 ;
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 A8, A6, A9, A14, A13, A12, A11, A10; :: thesis: verum
end;
then Intersect FF <> {} by ;
then consider m being object such that
A19: 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 ;
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 A20: 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)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (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 ;
then A21: 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)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (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 ;
then A22: 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)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (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 ;
then A23: 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)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (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 ;
then A24: 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)))) +* (M .--> (EqClass (u,M)))) +* (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)))) +* (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 ;
then A25: m in (((((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (u,J)) by ;
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 ;
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 ;
then A26: m in ((((((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (u,J))) /\ (EqClass (u,M)) by ;
m in EqClass (z,A) by ;
hence (EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M))) /\ (EqClass (z,A)) <> {} by ; :: thesis: verum