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 Th17, Th19; :: 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
thus X c= Y /\ Z by A1, Th19; :: according to PBOOLE:def 13 :: thesis: Y /\ Z c= X
( Y /\ Z c= Y & Y /\ Z c= Z implies Y /\ Z c= X ) by A2;
hence Y /\ Z c= X by Th17; :: thesis: verum