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
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;