let S1 be OrderSortedSign; 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; 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; 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; ( s1 <= s2 implies OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1) )
assume A1:
s1 <= s2
; 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 )
hence
OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1)
by SETFAM_1:def 3; verum