theorem
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C being
a_partition of
Y for
z,
u being
Element of
Y st
G is
independent &
G = {A,B,C} &
A <> B &
B <> C &
C <> A &
EqClass (
z,
C)
= EqClass (
u,
C) holds
EqClass (
u,
(CompF (A,G)))
meets EqClass (
z,
(CompF (B,G)))