let S be OrderSortedSign; :: thesis: for M being MSAlgebra of S holds
( M is order-sorted iff the Sorts of M is OrderSortedSet of )
let M be MSAlgebra of S; :: thesis: ( M is order-sorted iff the Sorts of M is OrderSortedSet of )
set So = the Sorts of M;
reconsider So1 = the Sorts of M as ManySortedSet of ;
thus ( M is order-sorted implies the Sorts of M is OrderSortedSet of ) :: thesis: ( the Sorts of M is OrderSortedSet of implies M is order-sorted )

proof

assume A1: M is order-sorted ; :: thesis: the Sorts of M is OrderSortedSet of
So1 is order-sorted

proof

let s1 be SortSymbol of S; :: according to OSALG_1:def 18 :: thesis: for s2 being Element of S st s1 <= s2 holds
So1 . s1 c= So1 . s2
let s2 be SortSymbol of S; :: thesis: ( s1 <= s2 implies So1 . s1 c= So1 . s2 )
thus ( s1 <= s2 implies So1 . s1 c= So1 . s2 ) by A1, Def19; :: thesis: verum

end;

hence the Sorts of M is OrderSortedSet of ; :: thesis: verum

end;

assume A2: the Sorts of M is OrderSortedSet of ; :: thesis: M is order-sorted
let s1 be SortSymbol of S; :: according to OSALG_1:def 19 :: thesis: for s2 being SortSymbol of S st s1 <= s2 holds
the Sorts of M . s1 c= the Sorts of M . s2
let s2 be SortSymbol of S; :: thesis: ( s1 <= s2 implies the Sorts of M . s1 c= the Sorts of M . s2 )
thus ( s1 <= s2 implies the Sorts of M . s1 c= the Sorts of M . s2 ) by A2, Def18; :: thesis: verum