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

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