set Sk = NAT --> {} ;
dom (NAT --> {} ) = NAT by FUNCOP_1:19;
then reconsider Sk = NAT --> {} as ManySortedSet of by PARTFUN1:def 4;
for n being Nat st not Sk . n is empty holds
for m being Nat st m < n holds
not Sk . m is empty

proof

let n be Nat; :: thesis: ( not Sk . n is empty implies for m being Nat st m < n holds
not Sk . m is empty )
A1: n in NAT by ORDINAL1:def 13;
assume not Sk . n is empty ; :: thesis: for m being Nat st m < n holds
not Sk . m is empty
hence for m being Nat st m < n holds
not Sk . m is empty by A1, FUNCOP_1:13; :: thesis: verum

end;

then A2: Sk is lower_non-empty by Def4;
consider A being ManySortedFunction of NatEmbSeq , FuncsSeq Sk;
take TriangStr(# Sk,A #) ; :: thesis: ( TriangStr(# Sk,A #) is lower_non-empty & TriangStr(# Sk,A #) is strict )
thus ( TriangStr(# Sk,A #) is lower_non-empty & TriangStr(# Sk,A #) is strict ) by A2, Def9; :: thesis: verum