let T be Nat; :: thesis: { w where w is Element of NAT : w <= T } is non empty Subset of NAT
B1: { w where w is Element of NAT : w <= T } c= NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of NAT : w <= T } or x in NAT )
assume x in { w where w is Element of NAT : w <= T } ; :: thesis: x in NAT
then consider w being Element of NAT such that
C1: ( x = w & w <= T ) ;
thus x in NAT by C1; :: thesis: verum

end;

T in { w where w is Element of NAT : w <= T }

proof

T in NAT by ORDINAL1:def 12;
hence T in { w where w is Element of NAT : w <= T } ; :: thesis: verum

end;

hence { w where w is Element of NAT : w <= T } is non empty Subset of NAT by B1; :: thesis: verum