let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds OSSubSort A c= OSSubSort OU0
let OU0 be OSAlgebra of S1; :: thesis: for A being OSSubset of OU0 holds OSSubSort A c= OSSubSort OU0
let A be OSSubset of OU0; :: thesis: OSSubSort A c= OSSubSort OU0
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in OSSubSort A or x in OSSubSort OU0 )
assume x in OSSubSort A ; :: thesis: x in OSSubSort OU0
then consider x1 being Element of SubSort A such that
A1: x1 = x and
A2: x1 is OrderSortedSet of S1 ;
( x1 in SubSort A & SubSort A c= SubSort OU0 ) by MSUALG_2:39;
then reconsider x2 = x1 as Element of SubSort OU0 ;
x2 in { y where y is Element of SubSort OU0 : y is OrderSortedSet of S1 } by A2;
hence x in OSSubSort OU0 by A1; :: thesis: verum