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 set ; :: 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 Th21;
hence x in SubSort A,s by A1, MSUALG_2:def 14; :: thesis: verum