set Sk = NAT --> {} ;
reconsider Sk = NAT --> {} as ManySortedSet of NAT ;
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 )
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 )
assume A1: not Sk . n is empty ; :: thesis: for m being Nat st m < n holds
not Sk . m is empty
n in NAT by ORDINAL1:def 13;
hence for m being Nat st m < n holds
not Sk . m is empty by A1, FUNCOP_1:13; :: thesis: verum

end;

then Sk is lower_non-empty by Def4;
hence ( TriangStr(# Sk,A #) is lower_non-empty & TriangStr(# Sk,A #) is strict ) by Def9; :: thesis: verum