let r be irrational Real; :: thesis: TRANQN .: (HWZSet r) = HWZSet1 r
thus TRANQN .: (HWZSet r) c= HWZSet1 r :: according to XBOOLE_0:def 10 :: thesis: HWZSet1 r c= TRANQN .: (HWZSet r)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in TRANQN .: (HWZSet r) or y in HWZSet1 r )
assume A2: y in TRANQN .: (HWZSet r) ; :: thesis: y in HWZSet1 r
consider p being object such that
A3: p in dom TRANQN and
A4: p in HWZSet r and
A5: y = TRANQN . p by A2, FUNCT_1:def 6;
consider q being Element of RAT such that
A6: q = p by A3;
y = denominator q by Def3A, A5, A6;
hence y in HWZSet1 r by A4, A6; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in HWZSet1 r or y in TRANQN .: (HWZSet r) )
assume y in HWZSet1 r ; :: thesis: y in TRANQN .: (HWZSet r)
then consider y1 being Nat such that
A11: y1 = y and
A12: ex p being Rational st
( p in HWZSet r & y1 = denominator p ) ;
consider p being Rational such that
A13: ( p in HWZSet r & y1 = denominator p ) by A12;
A14: dom TRANQN = RAT by FUNCT_2:def 1;
y1 = TRANQN . p by Def3A, A13;
hence y in TRANQN .: (HWZSet r) by A11, A13, A14, FUNCT_1:def 6; :: thesis: verum