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

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