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 Th14, Th16; :: 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 Th14;
then A3: X c= Y (\/) Z by A2;
Y (\/) Z c= X by A1, Th16;
hence X = Y (\/) Z by A3, Lm1; :: thesis: verum