let a, b be real number ; :: thesis: ( a < b implies IRRAT a,b misses RAT a,b )
assume A1: a < b ; :: thesis: IRRAT a,b misses RAT a,b
assume IRRAT a,b meets RAT a,b ; :: thesis: contradiction
then consider x being set such that
A2: ( x in IRRAT a,b & x in RAT a,b ) by XBOOLE_0:3;
reconsider x = x as real number by A2;
( not x is irrational & x is irrational ) by A1, A2, Th53;
hence contradiction ; :: thesis: verum