let Y be non empty set ; for G being Subset of (PARTITIONS Y)
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 (PARTITIONS Y); 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; 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; ( 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))
; 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 A3, Th49;
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 A3, Th49;
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 A3, Th49;
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 A3, Th49;
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 A3, Th49;
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 A3, Th49;
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 A3, Th49;
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 ;
TARSKI:def 3 ( 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))))
;
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 A16, ENUMSET1:def 5;
hence
t in bool Y
by A5, A10, A15, A14, A12, A11, A13;
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 A2, Th50;
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 A2, ENUMSET1:def 5;
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 ;
( 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
;
(((((((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 A2, ENUMSET1:def 5;
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;
verum
end;
then
Intersect FF <> {}
by A1, A17, BVFUNC_2:def 5;
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 A2, A17, ENUMSET1:def 5;
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 A15, A19, A20, 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)))) +* (A .--> (EqClass (z,A))))
by A2, A17, ENUMSET1:def 5;
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 A10, A19, A20, SETFAM_1:def 1;
then A22:
m in (EqClass (u,B)) /\ (EqClass (u,C))
by A21, 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)))) +* (A .--> (EqClass (z,A))))
by A2, A17, ENUMSET1:def 5;
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 A14, A19, A20, SETFAM_1:def 1;
then A23:
m in ((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))
by A22, 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)))) +* (A .--> (EqClass (z,A))))
by A2, A17, ENUMSET1:def 5;
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 A12, A19, A20, SETFAM_1:def 1;
then A24:
m in (((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))
by A23, 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)))) +* (A .--> (EqClass (z,A))))
by A2, A17, ENUMSET1:def 5;
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 A11, A19, A20, SETFAM_1:def 1;
then A25:
m in ((((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))
by A24, 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)))) +* (A .--> (EqClass (z,A))))
by A2, A17, ENUMSET1:def 5;
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 A13, A19, A20, 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))
by A25, XBOOLE_0:def 4;
m in EqClass (z,A)
by A5, A18, A19, A20, SETFAM_1:def 1;
then A27:
GG /\ I <> {}
by A6, A26, XBOOLE_0:def 4;
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 A27, SETFAM_1:def 5, TARSKI:def 1;
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 A28, XBOOLE_0:def 4;
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 A4, BVFUNC11:3;
then
K meets L
by A29, A30, XBOOLE_0:3;
then
K = L
by EQREL_1:41;
then A31:
z in K
by EQREL_1:def 6;
( p in K & p in I )
by A28, EQREL_1:def 6, XBOOLE_0:def 4;
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 SETFAM_1:def 5, TARSKI:def 1;
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 A31, XBOOLE_0:def 4;
then A34:
I /\ K meets HH
by A8, XBOOLE_0:3;
CompF (B,G) = ((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
by A2, A3, Th43;
then
p in HH
by A32, A33, A34, A9, EQREL_1:def 4;
hence
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))
by A7, A29, XBOOLE_0:3; verum