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