let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C being a_partition of Y st G = {A,B,C} & A <> B & B <> C holds
CompF (B,G) = C '/\' A
let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C being a_partition of Y st G = {A,B,C} & A <> B & B <> C holds
CompF (B,G) = C '/\' A
let A, B, C be a_partition of Y; :: thesis: ( G = {A,B,C} & A <> B & B <> C implies CompF (B,G) = C '/\' A )
{A,B,C} = {B,C,A} by ENUMSET1:59;
hence ( G = {A,B,C} & A <> B & B <> C implies CompF (B,G) = C '/\' A ) by Th4; :: thesis: verum