let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I holds
( X = Y /\ Z iff ( X c= Y & X c= Z & ( for V being ManySortedSet of I st V c= Y & V c= Z holds
V c= X ) ) )
let X, Y, Z be ManySortedSet of I; :: thesis: ( X = Y /\ Z iff ( X c= Y & X c= Z & ( for V being ManySortedSet of I st V c= Y & V c= Z holds
V c= X ) ) )
thus ( X = Y /\ Z implies ( X c= Y & X c= Z & ( for V being ManySortedSet of I st V c= Y & V c= Z holds
V c= X ) ) ) by Th15, Th17; :: thesis: ( X c= Y & X c= Z & ( for V being ManySortedSet of I 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 ManySortedSet of I st V c= Y & V c= Z holds
V c= X ; :: thesis: X = Y /\ Z
A3: X c= Y /\ Z by A1, Th17;
( Y /\ Z c= Y & Y /\ Z c= Z implies Y /\ Z c= X ) by A2;
hence X = Y /\ Z by A3, Lm1, Th15; :: thesis: verum