let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0
for s1, s2 being SortSymbol of S1 st s1 <= s2 holds
OSSubSort A,s2 is_coarser_than OSSubSort A,s1
let OU0 be OSAlgebra of S1; :: thesis: for A being OSSubset of OU0
for s1, s2 being SortSymbol of S1 st s1 <= s2 holds
OSSubSort A,s2 is_coarser_than OSSubSort A,s1
let A be OSSubset of OU0; :: thesis: for s1, s2 being SortSymbol of S1 st s1 <= s2 holds
OSSubSort A,s2 is_coarser_than OSSubSort A,s1
let s1, s2 be SortSymbol of S1; :: thesis: ( s1 <= s2 implies OSSubSort A,s2 is_coarser_than OSSubSort A,s1 )
assume A1: s1 <= s2 ; :: thesis: OSSubSort A,s2 is_coarser_than OSSubSort A,s1
for Y being set st Y in OSSubSort A,s2 holds
ex X being set st
( X in OSSubSort A,s1 & X c= Y )

proof

let x be set ; :: thesis: ( x in OSSubSort A,s2 implies ex X being set st
( X in OSSubSort A,s1 & X c= x ) )
assume x in OSSubSort A,s2 ; :: thesis: ex X being set st
( X in OSSubSort A,s1 & X c= x )
then consider B being OSSubset of OU0 such that
A2: ( B in OSSubSort A & x = B . s2 ) by Def10;
take B . s1 ; :: thesis: ( B . s1 in OSSubSort A,s1 & B . s1 c= x )
B is OrderSortedSet of S1 by Def2;
hence ( B . s1 in OSSubSort A,s1 & B . s1 c= x ) by A1, A2, Def10, OSALG_1:def 18; :: thesis: verum

end;

hence OSSubSort A,s2 is_coarser_than OSSubSort A,s1 by SETFAM_1:def 3; :: thesis: verum