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)

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

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 HWZSet1 r or y in TRANQN .: (HWZSet r) )
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;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

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