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 Th5;
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 set ; :: 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 Def12;
SO . s3 c= SO . s4 by A1, OSALG_1:def 18;
hence z in OSClass E,s2 by A2, A3, Def12; :: thesis: verum

end;