let X, Y be OrderSortedSet of S; :: thesis: ( ( for s1 being Element of S holds X . s1 = OSClass (E,s1) ) & ( for s1 being Element of S holds Y . s1 = OSClass (E,s1) ) implies X = Y )
assume A4: for s1 being Element of S holds X . s1 = OSClass (E,s1) ; :: thesis: ( ex s1 being Element of S st not Y . s1 = OSClass (E,s1) or X = Y )
assume A5: for s1 being Element of S holds Y . s1 = OSClass (E,s1) ; :: thesis: X = Y

now :: thesis: for s1 being object st s1 in the carrier of S holds
X . s1 = Y . s1

let s1 be object ; :: thesis: ( s1 in the carrier of S implies X . s1 = Y . s1 )
assume s1 in the carrier of S ; :: thesis: X . s1 = Y . s1
then reconsider s2 = s1 as Element of S ;
thus X . s1 = OSClass (E,s2) by A4
.= Y . s1 by A5 ; :: thesis: verum

end;

hence X = Y by PBOOLE:3; :: thesis: verum