let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M, N 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,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N holds
(EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) /\ (EqClass z,A) <> {}
let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C, D, E, F, J, M, N 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,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N holds
(EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) /\ (EqClass z,A) <> {}
let A, B, C, D, E, F, J, M, N 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,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N holds
(EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) /\ (EqClass z,A) <> {}
let z, u be Element of Y; :: thesis: ( G is independent & G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N implies (EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) /\ (EqClass z,A) <> {} )
assume that
A1: G is independent and
A2: G = {A,B,C,D,E,F,J,M,N} and
A3: ( A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N ) ; :: thesis: (EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) /\ (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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A));
A4: (((((((((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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . A = EqClass z,A by A3, Th88;
set GG = EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N);
EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = (EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) /\ (EqClass u,N) by Th1;
then EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = ((EqClass u,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J)) /\ (EqClass u,M)) /\ (EqClass u,N) by Th1;
then EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = (((EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) /\ (EqClass u,J)) /\ (EqClass u,M)) /\ (EqClass u,N) by Th1;
then EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = ((((EqClass u,(((B '/\' C) '/\' D) '/\' E)) /\ (EqClass u,F)) /\ (EqClass u,J)) /\ (EqClass u,M)) /\ (EqClass u,N) by Th1;
then EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = (((((EqClass u,((B '/\' C) '/\' D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass u,J)) /\ (EqClass u,M)) /\ (EqClass u,N) by Th1;
then EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = ((((((EqClass u,(B '/\' C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass u,J)) /\ (EqClass u,M)) /\ (EqClass u,N) by Th1;
then A5: (EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) /\ (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 u,N)) /\ (EqClass z,A) by Th1;
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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . B = EqClass u,B by A3, Th88;
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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . F = EqClass u,F by A3, Th88;
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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . E = EqClass u,E by A3, Th88;
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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . M = EqClass u,M by A3, Th88;
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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . J = EqClass u,J by A3, Th88;
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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . N = EqClass u,N by A3, Th88;
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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . D = EqClass u,D by A3, Th88;
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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . C = EqClass u,C by A3, Th88;
A14: 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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . M),((((((((((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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . N)} by Th90;
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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) c= bool Y

proof

let t be set ; :: 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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . M 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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . N ) by A14, ENUMSET1:def 7;
hence t in bool Y by A4, A6, A13, A12, A8, A7, A10, A9, A11; :: 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))) +* (N .--> (EqClass u,N))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) = G by A2, Th89;
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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) by A2, ENUMSET1:def 7;
then 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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))) by SETFAM_1:def 10;
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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (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 or d = N ) by A2, ENUMSET1:def 7;
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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . d in d by A4, A6, A13, A12, A8, A7, A10, A9, A11; :: thesis: verum

end;

then Intersect FF <> {} by A1, A15, BVFUNC_2:def 5;
then consider m being set such that
A18: 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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) by A2, A15, ENUMSET1:def 7;
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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then A19: m in EqClass u,C by A13, A17, A18, 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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) by A2, A15, ENUMSET1:def 7;
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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in EqClass u,B by A6, A17, A18, SETFAM_1:def 1;
then A20: m in (EqClass u,B) /\ (EqClass u,C) by A19, 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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) by A2, A15, ENUMSET1:def 7;
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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in EqClass u,D by A12, A17, A18, SETFAM_1:def 1;
then A21: m in ((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D) by A20, 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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) by A2, A15, ENUMSET1:def 7;
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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in EqClass u,E by A8, A17, A18, SETFAM_1:def 1;
then A22: m in (((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E) by A21, 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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) by A2, A15, ENUMSET1:def 7;
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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in EqClass u,F by A7, A17, A18, SETFAM_1:def 1;
then A23: m in ((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F) by A22, 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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) by A2, A15, ENUMSET1:def 7;
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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in EqClass u,J by A10, A17, A18, SETFAM_1:def 1;
then A24: m in (((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass u,J) by A23, 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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) by A2, A15, ENUMSET1:def 7;
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))) +* (N .--> (EqClass u,N))) +* (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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in EqClass u,M by A9, A17, A18, SETFAM_1:def 1;
then A25: m in ((((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass u,J)) /\ (EqClass u,M) by A24, XBOOLE_0:def 4;
N 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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) by A2, A15, ENUMSET1:def 7;
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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . N 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))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in EqClass u,N by A11, A17, A18, SETFAM_1:def 1;
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)) /\ (EqClass u,N) by A25, XBOOLE_0:def 4;
m in EqClass z,A by A4, A16, A17, A18, SETFAM_1:def 1;
hence (EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) /\ (EqClass z,A) <> {} by A5, A26, XBOOLE_0:def 4; :: thesis: verum