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 & EqClass (z,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) = EqClass (u,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) 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, 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 & EqClass (z,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) = EqClass (u,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))
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 & EqClass (z,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) = EqClass (u,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) 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,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 & EqClass (z,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) = EqClass (u,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) 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,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 ) and
A4: EqClass (z,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) = EqClass (u,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) ; :: 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)))) +* (N .--> (EqClass (u,N)))) +* (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)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . A = EqClass (z,A) by A3, Th76;
set L = EqClass (z,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N));
set GG = EqClass (u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N));
reconsider I = EqClass (z,A) as set ;
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 A6: (EqClass (u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N))) /\ I = ((((((((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;
A7: CompF (A,G) = ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N by A2, A3, Th67;
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) '/\' M) '/\' N) = (A '/\' (((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) '/\' N by PARTIT1:14
.= ((A '/\' ((((C '/\' D) '/\' E) '/\' F) '/\' J)) '/\' M) '/\' N by PARTIT1:14
.= (((A '/\' (((C '/\' D) '/\' E) '/\' F)) '/\' J) '/\' M) '/\' N by PARTIT1:14
.= ((((A '/\' ((C '/\' D) '/\' E)) '/\' F) '/\' J) '/\' M) '/\' N by PARTIT1:14
.= (((((A '/\' (C '/\' D)) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N by PARTIT1:14
.= ((((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N 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)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . B = EqClass (u,B) by A3, Th76;
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, Th76;
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, Th76;
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, Th76;
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)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . M = EqClass (u,M) by A3, Th76;
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)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . J = EqClass (u,J) by A3, Th76;
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)))) . F = EqClass (u,F) by A3, Th76;
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)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . E = EqClass (u,E) by A3, Th76;
A18: 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 Th78;
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 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)))) +* (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 A18, ENUMSET1:def 7;
hence t in bool Y by A5, A10, A13, A12, A17, A16, A15, A14, 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 ;
A19: 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, Th77;
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 A20: (((((((((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 3;
then A21: 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 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)))) +* (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 A5, A10, A13, A12, A17, A16, A15, A14, A11; :: thesis: verum

end;

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