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 that

A4: for s being SortSymbol of S holds W1 . s = meet (SubSort (A,s)) and

A5: for s being SortSymbol of S holds W2 . s = meet (SubSort (A,s)) ; :: thesis: W1 = W2

for s being object st s in the carrier of S holds

W1 . s = W2 . s

assume that

A4: for s being SortSymbol of S holds W1 . s = meet (SubSort (A,s)) and

A5: for s being SortSymbol of S holds W2 . s = meet (SubSort (A,s)) ; :: thesis: W1 = W2

for s being object st s in the carrier of S holds

W1 . s = W2 . s

proof

hence
W1 = W2
; :: thesis: verum
let s be object ; :: 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)) by A4;

hence W1 . s = W2 . s by A5; :: thesis: verum

end;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)) by A4;

hence W1 . s = W2 . s by A5; :: thesis: verum