let k be natural number ; :: thesis: k = { i where i is Element of NAT : i < k }
thus k c= { i where i is Element of NAT : i < k } :: according to XBOOLE_0:def 10 :: thesis: { i where i is Element of NAT : i < k } c= k

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in k or e in { i where i is Element of NAT : i < k } )
reconsider k' = k as Element of NAT by ORDINAL1:def 13;
A1: k' c= NAT by ORDINAL1:def 2;
assume A2: e in k ; :: thesis: e in { i where i is Element of NAT : i < k }
then reconsider j = e as Element of NAT by A1;
k' in NAT ;
then reconsider x' = k' as Element of REAL+ by ARYTM_2:2;
e in NAT by A1, A2;
then reconsider y' = e as Element of REAL+ by ARYTM_2:2;
y' in x' by A2;
then A3: ( y' in NAT & y' <> x' & y' <=' x' ) by ARYTM_2:19;
then j <= k by Lm1;
then j < k by A3, XXREAL_0:1;
hence e in { i where i is Element of NAT : i < k } ; :: thesis: verum

end;

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { i where i is Element of NAT : i < k } or e in k )
assume e in { i where i is Element of NAT : i < k } ; :: thesis: e in k
then consider i being Element of NAT such that
A4: e = i and
A5: not k <= i ;
A6: ( k in NAT & i in NAT ) by ORDINAL1:def 13;
then reconsider x' = e, y' = k as Element of REAL+ by A4, ARYTM_2:2;
not y' <=' x' by A4, A5, Lm1;
hence e in k by A4, A5, A6, ARYTM_2:19; :: thesis: verum