let W1, W2 be MSSubset of U0; :: thesis: ( ( for s being SortSymbol of S holds W1 . s = meet (SubSort A,s) ) & ( for s being SortSymbol of S holds W2 . s = meet (SubSort A,s) ) implies W1 = W2 )
assume A3: ( ( for s being SortSymbol of S holds W1 . s = meet (SubSort A,s) ) & ( for s being SortSymbol of S holds W2 . s = meet (SubSort A,s) ) ) ; :: thesis: W1 = W2
for s being set st s in the carrier of S holds
W1 . s = W2 . s

proof

let s be set ; :: thesis: ( s in the carrier of S implies W1 . s = W2 . s )
assume s in the carrier of S ; :: thesis: W1 . s = W2 . s
then reconsider s = s as SortSymbol of S ;
( W1 . s = meet (SubSort A,s) & W2 . s = meet (SubSort A,s) ) by A3;
hence W1 . s = W2 . s ; :: thesis: verum

end;

hence W1 = W2 by PBOOLE:3; :: thesis: verum