let S1 be OrderSortedSign; for M being ManySortedSet of the carrier of S1
for A being OrderSortedSet of S1 st M c= A holds
OSCl M c= A
let M be ManySortedSet of the carrier of S1; for A being OrderSortedSet of S1 st M c= A holds
OSCl M c= A
let A be OrderSortedSet of S1; ( M c= A implies OSCl M c= A )
assume A1:
M c= A
; OSCl M c= A
assume
not OSCl M c= A
; contradiction
then consider i being object such that
A2:
i in the carrier of S1
and
A3:
not (OSCl M) . i c= A . i
;
reconsider s = i as SortSymbol of S1 by A2;
consider x being object such that
A4:
x in (OSCl M) . i
and
A5:
not x in A . i
by A3;
(OSCl M) . s = union { (M . s2) where s2 is SortSymbol of S1 : s2 <= s }
by Def4;
then consider X1 being set such that
A6:
x in X1
and
A7:
X1 in { (M . s2) where s2 is SortSymbol of S1 : s2 <= s }
by A4, TARSKI:def 4;
consider s1 being SortSymbol of S1 such that
A8:
X1 = M . s1
and
A9:
s1 <= s
by A7;
M . s1 c= A . s1
by A1;
then A10:
x in A . s1
by A6, A8;
A . s1 c= A . s
by A9, OSALG_1:def 16;
hence
contradiction
by A5, A10; verum