let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I holds
( X = Y \/ Z iff ( Y c= X & Z c= X & ( for V being ManySortedSet of I st Y c= V & Z c= V holds
X c= V ) ) )
let X, Y, Z be ManySortedSet of I; :: thesis: ( X = Y \/ Z iff ( Y c= X & Z c= X & ( for V being ManySortedSet of I st Y c= V & Z c= V holds
X c= V ) ) )
thus ( X = Y \/ Z implies ( Y c= X & Z c= X & ( for V being ManySortedSet of I st Y c= V & Z c= V holds
X c= V ) ) ) by Th16, Th18; :: thesis: ( Y c= X & Z c= X & ( for V being ManySortedSet of I 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 ManySortedSet of I st Y c= V & Z c= V holds
X c= V ; :: thesis: X = Y \/ Z
( Y c= Y \/ Z & Z c= Y \/ Z ) by Th16;
hence X c= Y \/ Z by A2; :: according to PBOOLE:def 10 :: thesis: Y \/ Z c= X
thus Y \/ Z c= X by A1, Th18; :: thesis: verum