let T be Nat; :: thesis: ( T > 0 implies { w where w is Element of NAT : ( w > 0 & w <= T ) } is non empty Subset of NAT )
assume A0: T > 0 ; :: thesis: { w where w is Element of NAT : ( w > 0 & w <= T ) } is non empty Subset of NAT
B1: { w where w is Element of NAT : ( w > 0 & 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 > 0 & w <= T ) } or x in NAT )
assume x in { w where w is Element of NAT : ( w > 0 & w <= T ) } ; :: thesis: x in NAT
then consider w being Element of NAT such that
C1: ( x = w & w > 0 & w <= T ) ;
thus x in NAT by C1; :: thesis: verum
end;
( 1 > 0 & 1 <= T )
proof
( T > 0 & T = 1 * T ) by A0;
hence ( 1 > 0 & 1 <= T ) by NAT_1:24; :: thesis: verum
end;
then 1 in { w where w is Element of NAT : ( w > 0 & w <= T ) } ;
hence { w where w is Element of NAT : ( w > 0 & w <= T ) } is non empty Subset of NAT by B1; :: thesis: verum