theorem
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M 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} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
D <> E &
D <> F &
D <> J &
D <> M &
E <> F &
E <> J &
E <> M &
F <> J &
F <> M &
J <> M &
EqClass (
z,
(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M))
= EqClass (
u,
(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) holds
EqClass (
u,
(CompF (A,G)))
meets EqClass (
z,
(CompF (B,G)))