let W1, W2 be OrderSortedSet of S1; :: thesis: ( ( for s being SortSymbol of S1 holds W1 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ) & ( for s being SortSymbol of S1 holds W2 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ) implies W1 = W2 )
assume A6: for s being SortSymbol of S1 holds W1 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ; :: thesis: ( ex s being SortSymbol of S1 st not W2 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } or W1 = W2 )
assume A7: for s being SortSymbol of S1 holds W2 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ; :: thesis: W1 = W2
for s being object st s in the carrier of S1 holds
W1 . s = W2 . s

proof

let s be object ; :: thesis: ( s in the carrier of S1 implies W1 . s = W2 . s )
assume s in the carrier of S1 ; :: thesis: W1 . s = W2 . s
then reconsider t = s as SortSymbol of S1 ;
W1 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= t } by A6
.= W2 . s by A7 ;
hence W1 . s = W2 . s ; :: thesis: verum

end;

hence W1 = W2 ; :: thesis: verum