let a, b be Real; :: thesis: ( a < b implies ex c being Real st
( a < c & c < b ) )
assume A1: a < b ; :: thesis: ex c being Real st
( a < c & c < b )
take z = (a + b) / 2; :: thesis: ( a < z & z < b )
(1 * a) + a < a + b by A1, Lm10;
then (2 ") * (2 * a) < (2 ") * (a + b) by Lm13;
hence a < z ; :: thesis: z < b
a + b < (1 * b) + b by A1, Lm10;
then (2 ") * (a + b) < (2 ") * (2 * b) by Lm13;
hence z < b ; :: thesis: verum