let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C, D, E being a_partition of Y st G = {A,B,C,D,E} & A <> D & B <> D & C <> D & D <> E holds
CompF D,G = ((A '/\' B) '/\' C) '/\' E
let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C, D, E being a_partition of Y st G = {A,B,C,D,E} & A <> D & B <> D & C <> D & D <> E holds
CompF D,G = ((A '/\' B) '/\' C) '/\' E
let A, B, C, D, E be a_partition of Y; :: thesis: ( G = {A,B,C,D,E} & A <> D & B <> D & C <> D & D <> E implies CompF D,G = ((A '/\' B) '/\' C) '/\' E )
assume that
A1: G = {A,B,C,D,E} and
A2: ( A <> D & B <> D & C <> D & D <> E ) ; :: thesis: CompF D,G = ((A '/\' B) '/\' C) '/\' E
{A,B,C,D,E} = {A,B} \/ {C,D,E} by ENUMSET1:48;
then {A,B,C,D,E} = {A,B} \/ ({C,D} \/ {E}) by ENUMSET1:43;
then {A,B,C,D,E} = {A,B} \/ {D,C,E} by ENUMSET1:43;
then G = {A,B,D,C,E} by A1, ENUMSET1:48;
hence CompF D,G = ((A '/\' B) '/\' C) '/\' E by A2, Th26; :: thesis: verum