let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C, D, E 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} & A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E holds
EqClass (u,(((B '/\' C) '/\' D) '/\' E)) meets EqClass (z,A)
let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C, D, E 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} & A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E holds
EqClass (u,(((B '/\' C) '/\' D) '/\' E)) meets EqClass (z,A)
let A, B, C, D, E 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} & A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E holds
EqClass (u,(((B '/\' C) '/\' D) '/\' E)) meets EqClass (z,A)
let z, u be Element of Y; :: thesis: for h being Function st G is independent & G = {A,B,C,D,E} & A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E holds
EqClass (u,(((B '/\' C) '/\' D) '/\' E)) meets EqClass (z,A)
let h be Function; :: thesis: ( G is independent & G = {A,B,C,D,E} & A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E implies EqClass (u,(((B '/\' C) '/\' D) '/\' E)) meets EqClass (z,A) )
assume that
A1: G is independent and
A2: G = {A,B,C,D,E} and
A3: ( A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E ) ; :: thesis: EqClass (u,(((B '/\' C) '/\' D) '/\' E)) meets EqClass (z,A)
set h = ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)));
A4: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . B = EqClass (u,B) by A3, Th26;
A5: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . D = EqClass (u,D) by A3, Th26;
A6: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . C = EqClass (u,C) by A3, Th26;
A7: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . E = EqClass (u,E) by A3, Th26;
A8: rng (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) = {((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . A),((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . B),((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . C),((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . D),((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . E)} by Th28;
rng (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (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)))) +* (A .--> (EqClass (z,A)))) or t in bool Y )
assume A9: t in rng (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) ; :: thesis: t in bool Y

now :: thesis: ( ( t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . A & t in bool Y ) or ( t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . B & t in bool Y ) or ( t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . C & t in bool Y ) or ( t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . D & t in bool Y ) or ( t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . E & t in bool Y ) )

per cases ( t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . A or t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . B or t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . C or t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . D or t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . E ) by A8, A9, ENUMSET1:def 3;

case t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . A ; :: thesis: t in bool Y

then t = EqClass (z,A) by A3, Th26;
hence t in bool Y ; :: thesis: verum

end;

case t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . B ; :: thesis: t in bool Y

hence t in bool Y by A4; :: thesis: verum

end;

case t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . C ; :: thesis: t in bool Y

hence t in bool Y by A6; :: thesis: verum

end;

case t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . D ; :: thesis: t in bool Y

hence t in bool Y by A5; :: thesis: verum

end;

case t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . E ; :: thesis: t in bool Y

hence t in bool Y by A7; :: thesis: verum

end;

end;

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)))) +* (A .--> (EqClass (z,A)))) as Subset-Family of Y ;
A10: dom (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) = G by A2, Th27;
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)))) +* (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)))) +* (A .--> (EqClass (z,A)))) . d in d )
assume A11: d in G ; :: thesis: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d

now :: thesis: ( ( d = A & (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d ) or ( d = B & (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d ) or ( d = C & (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d ) or ( d = D & (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d ) or ( d = E & (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d ) )

per cases ( d = A or d = B or d = C or d = D or d = E ) by A2, A11, ENUMSET1:def 3;

case A12: d = A ; :: thesis: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d

(((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . A = EqClass (z,A) by A3, Th26;
hence (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d by A12; :: thesis: verum

end;

case A13: d = B ; :: thesis: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d

(((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . B = EqClass (u,B) by A3, Th26;
hence (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d by A13; :: thesis: verum

end;

case A14: d = C ; :: thesis: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d

(((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . C = EqClass (u,C) by A3, Th26;
hence (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d by A14; :: thesis: verum

end;

case A15: d = D ; :: thesis: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d

(((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . D = EqClass (u,D) by A3, Th26;
hence (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d by A15; :: thesis: verum

end;

case A16: d = E ; :: thesis: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d

(((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . E = EqClass (u,E) by A3, Th26;
hence (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d by A16; :: thesis: verum

end;

end;

end;

hence (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d ; :: thesis: verum

end;

then Intersect FF <> {} by A1, A10, BVFUNC_2:def 5;
then consider m being object such that
A17: m in Intersect FF by XBOOLE_0:def 1;
A in dom (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by A2, A10, ENUMSET1:def 3;
then A18: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . A in rng (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then A19: m in meet FF by A17, SETFAM_1:def 9;
then A20: m in (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . A by A18, SETFAM_1:def 1;
D in dom (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by A2, A10, ENUMSET1:def 3;
then (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . D in rng (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then A21: m in (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . D by A19, SETFAM_1:def 1;
C in dom (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by A2, A10, ENUMSET1:def 3;
then (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . C in rng (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then A22: m in (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . C by A19, SETFAM_1:def 1;
B in dom (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by A2, A10, ENUMSET1:def 3;
then (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . B in rng (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . B by A19, SETFAM_1:def 1;
then m in (EqClass (u,B)) /\ (EqClass (u,C)) by A4, A6, A22, XBOOLE_0:def 4;
then A23: m in ((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D)) by A5, A21, XBOOLE_0:def 4;
E in dom (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by A2, A10, ENUMSET1:def 3;
then (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . E in rng (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . E by A19, SETFAM_1:def 1;
then A24: m in (((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E)) by A7, A23, XBOOLE_0:def 4;
set GG = EqClass (u,(((B '/\' C) '/\' D) '/\' E));
EqClass (u,(((B '/\' C) '/\' D) '/\' E)) = (EqClass (u,((B '/\' C) '/\' D))) /\ (EqClass (u,E)) by Th1;
then A25: EqClass (u,(((B '/\' C) '/\' D) '/\' E)) = ((EqClass (u,(B '/\' C))) /\ (EqClass (u,D))) /\ (EqClass (u,E)) by Th1;
(((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . A = EqClass (z,A) by A3, Th26;
then m in ((((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (z,A)) by A20, A24, XBOOLE_0:def 4;
then (((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E)) meets EqClass (z,A) by XBOOLE_0:4;
hence EqClass (u,(((B '/\' C) '/\' D) '/\' E)) meets EqClass (z,A) by A25, Th1; :: thesis: verum