let T be Element of 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 ) } is Subset of NAT

proof

for x being object st x in { w where w is Element of NAT : ( w > 0 & w <= T ) } holds
x in NAT

proof

let x be object ; :: thesis: ( x in { w where w is Element of NAT : ( w > 0 & w <= T ) } implies 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;

hence { w where w is Element of NAT : ( w > 0 & w <= T ) } is Subset of NAT by TARSKI:def 3; :: 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