let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0
for s being SortSymbol of S1 holds OSSubSort (A,s) c= SubSort (A,s)
let OU0 be OSAlgebra of S1; :: thesis: for A being OSSubset of OU0
for s being SortSymbol of S1 holds OSSubSort (A,s) c= SubSort (A,s)
let A be OSSubset of OU0; :: thesis: for s being SortSymbol of S1 holds OSSubSort (A,s) c= SubSort (A,s)
let s be SortSymbol of S1; :: thesis: OSSubSort (A,s) c= SubSort (A,s)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in OSSubSort (A,s) or x in SubSort (A,s) )
assume x in OSSubSort (A,s) ; :: thesis: x in SubSort (A,s)
then A1: ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) by Def10;
OSSubSort A c= SubSort A by Th16;
hence x in SubSort (A,s) by A1, MSUALG_2:def 13; :: thesis: verum