let S be locally_directed OrderSortedSign; :: thesis: for A being OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of A
for s1, s2 being Element of S st s1 <= s2 holds
OSClass (E,s1) c= OSClass (E,s2)
let A be OSAlgebra of S; :: thesis: for E being MSEquivalence-like OrderSortedRelation of A
for s1, s2 being Element of S st s1 <= s2 holds
OSClass (E,s1) c= OSClass (E,s2)
let E be MSEquivalence-like OrderSortedRelation of A; :: thesis: for s1, s2 being Element of S st s1 <= s2 holds
OSClass (E,s1) c= OSClass (E,s2)
let s1, s2 be Element of S; :: thesis: ( s1 <= s2 implies OSClass (E,s1) c= OSClass (E,s2) )
reconsider s3 = s1, s4 = s2 as Element of S ;
assume A1: s1 <= s2 ; :: thesis: OSClass (E,s1) c= OSClass (E,s2)
then A2: CComp s1 = CComp s2 by Th4;
thus OSClass (E,s1) c= OSClass (E,s2) :: thesis: verum

proof

reconsider SO = the Sorts of A as OrderSortedSet of S by OSALG_1:17;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in OSClass (E,s1) or z in OSClass (E,s2) )
assume z in OSClass (E,s1) ; :: thesis: z in OSClass (E,s2)
then A3: ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) by Def10;
SO . s3 c= SO . s4 by A1, OSALG_1:def 16;
hence z in OSClass (E,s2) by A2, A3, Def10; :: thesis: verum

end;