let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds OSSubSort A c= SubSort A
let OU0 be OSAlgebra of S1; :: thesis: for A being OSSubset of OU0 holds OSSubSort A c= SubSort A
let A be OSSubset of OU0; :: thesis: OSSubSort A c= SubSort A
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in OSSubSort A or x in SubSort A )
assume x in OSSubSort A ; :: thesis: x in SubSort A
then ex y being Element of SubSort A st
( x = y & y is OrderSortedSet of S1 ) ;
hence x in SubSort A ; :: thesis: verum