defpred S_{1}[ Nat] means ex p being Rational st

( p in HWZSet r & $1 = denominator p );

{ x where x is Nat : S_{1}[x] } c= NAT

( p in HWZSet r & x = denominator p ) } is Subset of NAT ; :: thesis: verum

( p in HWZSet r & $1 = denominator p );

{ x where x is Nat : S

proof

hence
{ x where x is Nat : ex p being Rational st
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Nat : S_{1}[x] } or y in NAT )

assume y in { x where x is Nat : S_{1}[x] }
; :: thesis: y in NAT

then ex x being Nat st

( y = x & S_{1}[x] )
;

hence y in NAT by ORDINAL1:def 12; :: thesis: verum

end;assume y in { x where x is Nat : S

then ex x being Nat st

( y = x & S

hence y in NAT by ORDINAL1:def 12; :: thesis: verum

( p in HWZSet r & x = denominator p ) } is Subset of NAT ; :: thesis: verum