let a, b be real number ; :: thesis: ( a < b implies ex p1, p2 being rational number st
( a < p1 & p1 < p2 & p2 < b ) )
assume a < b ; :: thesis: ex p1, p2 being rational number st
( a < p1 & p1 < p2 & p2 < b )
then consider p1 being rational number such that
A1: ( a < p1 & p1 < b ) by RAT_1:22;
consider p2 being rational number such that
A2: ( p1 < p2 & p2 < b ) by A1, RAT_1:22;
thus ex p1, p2 being rational number st
( a < p1 & p1 < p2 & p2 < b ) by A1, A2; :: thesis: verum