let x, a, b be Real; :: thesis: ( x in ].a,b.[ implies ex p, r being Rational st

( x in ].p,r.[ & ].p,r.[ c= ].a,b.[ ) )

assume A1: x in ].a,b.[ ; :: thesis: ex p, r being Rational st

( x in ].p,r.[ & ].p,r.[ c= ].a,b.[ )

A2: ( x > a & x < b ) by XXREAL_1:4, A1;

consider p being Rational such that

A3: ( p > a & x > p ) by A2, RAT_1:7;

consider r being Rational such that

A4: ( x < r & r < b ) by A2, RAT_1:7;

take p ; :: thesis: ex r being Rational st

( x in ].p,r.[ & ].p,r.[ c= ].a,b.[ )

take r ; :: thesis: ( x in ].p,r.[ & ].p,r.[ c= ].a,b.[ )

thus x in ].p,r.[ by A3, A4, XXREAL_1:4; :: thesis: ].p,r.[ c= ].a,b.[

thus ].p,r.[ c= ].a,b.[ :: thesis: verum

( x in ].p,r.[ & ].p,r.[ c= ].a,b.[ ) )

assume A1: x in ].a,b.[ ; :: thesis: ex p, r being Rational st

( x in ].p,r.[ & ].p,r.[ c= ].a,b.[ )

A2: ( x > a & x < b ) by XXREAL_1:4, A1;

consider p being Rational such that

A3: ( p > a & x > p ) by A2, RAT_1:7;

consider r being Rational such that

A4: ( x < r & r < b ) by A2, RAT_1:7;

take p ; :: thesis: ex r being Rational st

( x in ].p,r.[ & ].p,r.[ c= ].a,b.[ )

take r ; :: thesis: ( x in ].p,r.[ & ].p,r.[ c= ].a,b.[ )

thus x in ].p,r.[ by A3, A4, XXREAL_1:4; :: thesis: ].p,r.[ c= ].a,b.[

thus ].p,r.[ c= ].a,b.[ :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in ].p,r.[ or y in ].a,b.[ )

assume A5: y in ].p,r.[ ; :: thesis: y in ].a,b.[

then reconsider y1 = y as Element of REAL ;

( y1 > p & y1 < r ) by XXREAL_1:4, A5;

then ( y1 > a & y1 < b ) by A3, A4, XXREAL_0:2;

hence y in ].a,b.[ by XXREAL_1:4; :: thesis: verum

end;assume A5: y in ].p,r.[ ; :: thesis: y in ].a,b.[

then reconsider y1 = y as Element of REAL ;

( y1 > p & y1 < r ) by XXREAL_1:4, A5;

then ( y1 > a & y1 < b ) by A3, A4, XXREAL_0:2;

hence y in ].a,b.[ by XXREAL_1:4; :: thesis: verum