let k be Nat; :: thesis: k = { i where i is Nat : i < k }
A1: k in NAT by ORDINAL1:def 12;
thus k c= { i where i is Nat : i < k } :: according to XBOOLE_0:def 10 :: thesis: { i where i is Nat : i < k } c= k

proof

reconsider k9 = k as Element of NAT by ORDINAL1:def 12;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in k or e in { i where i is Nat : i < k } )
assume A2: e in k ; :: thesis: e in { i where i is Nat : i < k }
A3: k9 c= NAT by ORDINAL1:def 2;
then reconsider j = e as Element of NAT by A2;
e in NAT by A3, A2;
then reconsider y9 = e as Element of REAL+ by ARYTM_2:2;
reconsider x9 = k9 as Element of REAL+ by ARYTM_2:2;
y9 <=' x9 by A2, ARYTM_2:18;
then A4: j <= k by Lm1;
reconsider yy9 = y9 as set ;
not yy9 in yy9 ;
then y9 <> x9 by A2;
then j < k by A4, XXREAL_0:1;
hence e in { i where i is Nat : i < k } ; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { i where i is Nat : i < k } or e in k )
assume e in { i where i is Nat : i < k } ; :: thesis: e in k
then consider i being Nat such that
A5: e = i and
A6: not k <= i ;
A7: i in NAT by ORDINAL1:def 12;
then reconsider x9 = e, y9 = k as Element of REAL+ by A5, A1, ARYTM_2:2;
not y9 <=' x9 by A5, A6, Lm1;
hence e in k by A5, A6, A1, A7, ARYTM_2:18; :: thesis: verum