let T be Nat; :: thesis: { w where w is Element of NAT : ( w > 0 & w <= T ) } c= { w where w is Element of NAT : w <= T }
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 { w where w is Element of NAT : w <= T } )
assume x in { w where w is Element of NAT : ( w > 0 & w <= T ) } ; :: thesis: x in { w where w is Element of NAT : w <= T }
then consider w being Element of NAT such that
B1: ( x = w & w > 0 & w <= T ) ;
thus x in { w where w is Element of NAT : w <= T } by B1; :: thesis: verum