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: verumproof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in OSClass E,s1 or z in OSClass E,s2 )
assume A3:
z in OSClass E,
s1
;
:: thesis: z in OSClass E,s2
consider x being
set such that A4:
(
x in the
Sorts of
A . s1 &
z = Class (CompClass E,(CComp s1)),
x )
by A3, Def12;
reconsider SO = the
Sorts of
A as
OrderSortedSet of
by OSALG_1:17;
SO . s3 c= SO . s4
by A1, OSALG_1:def 18;
hence
z in OSClass E,
s2
by A2, A4, Def12;
:: thesis: verum
end;