let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F being a_partition of Y
for z, u being Element of Y
for h being Function st G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & EqClass z,(((C '/\' D) '/\' E) '/\' F) = EqClass u,(((C '/\' D) '/\' E) '/\' F) 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 being a_partition of Y
for z, u being Element of Y
for h being Function st G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & EqClass z,(((C '/\' D) '/\' E) '/\' F) = EqClass u,(((C '/\' D) '/\' E) '/\' F) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
let A, B, C, D, E, F be a_partition of Y; :: thesis: for z, u being Element of Y
for h being Function st G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & EqClass z,(((C '/\' D) '/\' E) '/\' F) = EqClass u,(((C '/\' D) '/\' E) '/\' F) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
let z, u be Element of Y; :: thesis: for h being Function st G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & EqClass z,(((C '/\' D) '/\' E) '/\' F) = EqClass u,(((C '/\' D) '/\' E) '/\' F) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
let h be Function; :: thesis: ( G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & EqClass z,(((C '/\' D) '/\' E) '/\' F) = EqClass u,(((C '/\' D) '/\' E) '/\' F) implies EqClass u,(CompF A,G) meets EqClass z,(CompF B,G) )
assume A1:
( G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & EqClass z,(((C '/\' D) '/\' E) '/\' F) = EqClass u,(((C '/\' D) '/\' E) '/\' F) )
; :: thesis: EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
then A2:
CompF B,G = (((A '/\' C) '/\' D) '/\' E) '/\' F
by Th35;
set H = EqClass z,(CompF B,G);
set I = EqClass z,A;
set GG = EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F);
A3:
EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F) = EqClass u,(CompF A,G)
by A1, Th34;
set h = (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A));
A4:
dom ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) = G
by A1, Th41;
A5:
((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . A = EqClass z,A
by A1, Th40;
A6:
((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . B = EqClass u,B
by A1, Th40;
A7:
((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . C = EqClass u,C
by A1, Th40;
A8:
((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . D = EqClass u,D
by A1, Th40;
A9:
((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . E = EqClass u,E
by A1, Th40;
A10:
((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . F = EqClass u,F
by A1, Th40;
A11:
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))) +* (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))) +* (A .--> (EqClass z,A))) . d in d )
assume A12:
d in G
;
:: thesis: ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . d in d
hence
((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . d in d
;
:: thesis: verum
end;
A in dom ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A)))
by A1, A4, ENUMSET1:def 4;
then A13:
((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (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))) +* (A .--> (EqClass z,A)))
by FUNCT_1:def 5;
B in dom ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A)))
by A1, A4, ENUMSET1:def 4;
then A14:
((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (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))) +* (A .--> (EqClass z,A)))
by FUNCT_1:def 5;
C in dom ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A)))
by A1, A4, ENUMSET1:def 4;
then A15:
((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (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))) +* (A .--> (EqClass z,A)))
by FUNCT_1:def 5;
D in dom ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A)))
by A1, A4, ENUMSET1:def 4;
then A16:
((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (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))) +* (A .--> (EqClass z,A)))
by FUNCT_1:def 5;
E in dom ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A)))
by A1, A4, ENUMSET1:def 4;
then A17:
((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (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))) +* (A .--> (EqClass z,A)))
by FUNCT_1:def 5;
F in dom ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A)))
by A1, A4, ENUMSET1:def 4;
then A18:
((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (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))) +* (A .--> (EqClass z,A)))
by FUNCT_1:def 5;
A19:
rng ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) = {(((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (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))) +* (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))) +* (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))) +* (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))) +* (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))) +* (A .--> (EqClass z,A))) . F)}
by A1, Th42;
rng ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (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))) +* (A .--> (EqClass z,A))) or t in bool Y )
assume A20:
t in rng ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A)))
;
:: thesis: t in bool Y
now per cases
( t = ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (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))) +* (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))) +* (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))) +* (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))) +* (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))) +* (A .--> (EqClass z,A))) . F )
by A19, A20, ENUMSET1:def 4;
end;
hence
t in bool Y
;
:: 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))) +* (A .--> (EqClass z,A))) as Subset-Family of Y ;
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))) +* (A .--> (EqClass z,A))))
by A13, SETFAM_1:def 10;
Intersect FF <> {}
by A1, A4, A11, BVFUNC_2:def 5;
then consider m being set such that
A22:
m in Intersect FF
by XBOOLE_0:def 1;
( m in ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . A & m in ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . B & m in ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . C & m in ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . D & m in ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . E & m in ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . F )
by A13, A14, A15, A16, A17, A18, A21, A22, SETFAM_1:def 1;
then A23:
( m in EqClass z,A & m in EqClass u,B & m in EqClass u,C & m in EqClass u,D & m in EqClass u,E & m in EqClass u,F )
by A1, Th40;
EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F) = (EqClass u,(((B '/\' C) '/\' D) '/\' E)) /\ (EqClass u,F)
by Th1;
then
EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F) = ((EqClass u,((B '/\' C) '/\' D)) /\ (EqClass u,E)) /\ (EqClass u,F)
by Th1;
then
EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F) = (((EqClass u,(B '/\' C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)
by Th1;
then A24:
(EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) /\ (EqClass z,A) = (((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass z,A)
by Th1;
m in (EqClass u,B) /\ (EqClass u,C)
by A23, XBOOLE_0:def 4;
then
m in ((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)
by A23, XBOOLE_0:def 4;
then
m in (((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)
by A23, XBOOLE_0:def 4;
then
m in ((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)
by A23, XBOOLE_0:def 4;
then
(EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) /\ (EqClass z,A) <> {}
by A23, A24, XBOOLE_0:def 4;
then consider p being set such that
A25:
p in (EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) /\ (EqClass z,A)
by XBOOLE_0:def 1;
reconsider p = p as Element of Y by A25;
set K = EqClass p,(((C '/\' D) '/\' E) '/\' F);
A26:
( p in EqClass p,(((C '/\' D) '/\' E) '/\' F) & EqClass p,(((C '/\' D) '/\' E) '/\' F) in ((C '/\' D) '/\' E) '/\' F )
by EQREL_1:def 8;
( p in EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F) & p in EqClass z,A )
by A25, XBOOLE_0:def 4;
then A27:
p in (EqClass z,A) /\ (EqClass p,(((C '/\' D) '/\' E) '/\' F))
by A26, XBOOLE_0:def 4;
then
( (EqClass z,A) /\ (EqClass p,(((C '/\' D) '/\' E) '/\' F)) in INTERSECTION A,(((C '/\' D) '/\' E) '/\' F) & not (EqClass z,A) /\ (EqClass p,(((C '/\' D) '/\' E) '/\' F)) in {{} } )
by SETFAM_1:def 5, TARSKI:def 1;
then
(EqClass z,A) /\ (EqClass p,(((C '/\' D) '/\' E) '/\' F)) in (INTERSECTION A,(((C '/\' D) '/\' E) '/\' F)) \ {{} }
by XBOOLE_0:def 5;
then A28:
(EqClass z,A) /\ (EqClass p,(((C '/\' D) '/\' E) '/\' F)) in A '/\' (((C '/\' D) '/\' E) '/\' F)
by PARTIT1:def 4;
set L = EqClass z,(((C '/\' D) '/\' E) '/\' F);
EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F) = EqClass u,(((B '/\' (C '/\' D)) '/\' E) '/\' F)
by PARTIT1:16;
then
EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F) = EqClass u,((B '/\' ((C '/\' D) '/\' E)) '/\' F)
by PARTIT1:16;
then
EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F) = EqClass u,(B '/\' (((C '/\' D) '/\' E) '/\' F))
by PARTIT1:16;
then A29:
EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F) c= EqClass z,(((C '/\' D) '/\' E) '/\' F)
by A1, BVFUNC11:3;
A30:
p in EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F)
by A25, XBOOLE_0:def 4;
p in EqClass p,(((C '/\' D) '/\' E) '/\' F)
by EQREL_1:def 8;
then
EqClass p,(((C '/\' D) '/\' E) '/\' F) meets EqClass z,(((C '/\' D) '/\' E) '/\' F)
by A29, A30, XBOOLE_0:3;
then
EqClass p,(((C '/\' D) '/\' E) '/\' F) = EqClass z,(((C '/\' D) '/\' E) '/\' F)
by EQREL_1:50;
then A31:
z in EqClass p,(((C '/\' D) '/\' E) '/\' F)
by EQREL_1:def 8;
z in EqClass z,A
by EQREL_1:def 8;
then A32:
z in (EqClass z,A) /\ (EqClass p,(((C '/\' D) '/\' E) '/\' F))
by A31, XBOOLE_0:def 4;
A33:
z in EqClass z,(CompF B,G)
by EQREL_1:def 8;
A '/\' (((C '/\' D) '/\' E) '/\' F) =
(A '/\' ((C '/\' D) '/\' E)) '/\' F
by PARTIT1:16
.=
((A '/\' (C '/\' D)) '/\' E) '/\' F
by PARTIT1:16
.=
(((A '/\' C) '/\' D) '/\' E) '/\' F
by PARTIT1:16
;
then
( (EqClass z,A) /\ (EqClass p,(((C '/\' D) '/\' E) '/\' F)) = EqClass z,(CompF B,G) or (EqClass z,A) /\ (EqClass p,(((C '/\' D) '/\' E) '/\' F)) misses EqClass z,(CompF B,G) )
by A2, A28, EQREL_1:def 6;
hence
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
by A3, A27, A30, A32, A33, XBOOLE_0:3; :: thesis: verum