theorem Th67:
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M,
N being
a_partition of
Y st
G = {A,B,C,D,E,F,J,M,N} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
A <> N &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
B <> N &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
C <> N &
D <> E &
D <> F &
D <> J &
D <> M &
D <> N &
E <> F &
E <> J &
E <> M &
E <> N &
F <> J &
F <> M &
F <> N &
J <> M &
J <> N &
M <> N holds
CompF (
A,
G)
= ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N