let a, b be real number ; :: 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
A1: x in IRRAT a,b and
A2: x in RAT a,b by XBOOLE_0:3;
thus contradiction by A1, A2, Th53; :: thesis: verum
reconsider x = x as real number by A1;