let S be locally_directed OrderSortedSign; 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; 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; 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; ( s1 <= s2 implies OSClass (E,s1) c= OSClass (E,s2) )
reconsider s3 = s1, s4 = s2 as Element of S ;
assume A1:
s1 <= s2
; OSClass (E,s1) c= OSClass (E,s2)
then A2:
CComp s1 = CComp s2
by Th4;
thus
OSClass (E,s1) c= OSClass (E,s2)
verumproof
reconsider SO = the
Sorts of
A as
OrderSortedSet of
S by OSALG_1:17;
let z be
object ;
TARSKI:def 3 ( not z in OSClass (E,s1) or z in OSClass (E,s2) )
assume
z in OSClass (
E,
s1)
;
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;
verum
end;