theorem Th4: :: BVFUNC14:4

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C being a_partition of Y st G = {A,B,C} & A <> B & C <> A holds
CompF (A,G) = B '/\' C