let k be natural Number ; :: thesis: k = { i where i is Nat : i < k }
A1: k in NAT by ORDINAL1:def 12;
set Y = { i where i is Nat : i < k } ;
reconsider K = k as Element of NAT by ORDINAL1:def 12;
for e being object holds
( e in K iff e in { i where i is Nat : i < k } )
proof
let e be object ; :: thesis: ( e in K iff e in { i where i is Nat : i < k } )
thus ( e in K implies e in { i where i is Nat : i < k } ) :: thesis: ( e in { i where i is Nat : i < k } implies e in K )
proof
assume A2: e in K ; :: thesis: e in { i where i is Nat : i < k }
A3: K 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 = K 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;
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, A7, ARYTM_2:18; :: thesis: verum
end;
hence k = { i where i is Nat : i < k } by TARSKI:2; :: thesis: verum