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 16; :: thesis: verum

end;

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