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