let X, Y, Z be set ; :: thesis: ( X c= Y & X c= Z & ( for V being set st V c= Y & V c= Z holds

V c= X ) implies X = Y /\ Z )

assume that

A1: ( X c= Y & X c= Z ) and

A2: for V being set st V c= Y & V c= Z holds

V c= X ; :: thesis: X = Y /\ Z

thus X c= Y /\ Z by A1, Th19; :: according to XBOOLE_0:def 10 :: thesis: Y /\ Z c= X

( Y /\ Z c= Y & Y /\ Z c= Z implies Y /\ Z c= X ) by A2;

hence Y /\ Z c= X by Th17; :: thesis: verum

V c= X ) implies X = Y /\ Z )

assume that

A1: ( X c= Y & X c= Z ) and

A2: for V being set st V c= Y & V c= Z holds

V c= X ; :: thesis: X = Y /\ Z

thus X c= Y /\ Z by A1, Th19; :: according to XBOOLE_0:def 10 :: thesis: Y /\ Z c= X

( Y /\ Z c= Y & Y /\ Z c= Z implies Y /\ Z c= X ) by A2;

hence Y /\ Z c= X by Th17; :: thesis: verum