theorem Th31:
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F being
a_partition of
Y st
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 holds
CompF (
A,
G)
= (((B '/\' C) '/\' D) '/\' E) '/\' F