let X, Y, Z be set ; :: thesis: ( Y c= X & Z c= X & ( for V being set st Y c= V & Z c= V holds
X c= V ) implies X = Y \/ Z )
assume that
A1: ( Y c= X & Z c= X ) and
A2: for V being set st Y c= V & Z c= V holds
X c= V ; :: thesis: X = Y \/ Z
( Y c= Y \/ Z & Z c= Y \/ Z ) by Th7;
hence X c= Y \/ Z by A2; :: according to XBOOLE_0:def 10 :: thesis: Y \/ Z c= X
thus Y \/ Z c= X by A1, Th8; :: thesis: verum