let a, b be Real; :: thesis: IRRAT (a,b) misses RAT (a,b)
assume IRRAT (a,b) meets RAT (a,b) ; :: thesis: contradiction
then consider x being object such that
A1: x in IRRAT (a,b) and
A2: x in RAT (a,b) by XBOOLE_0:3;
thus contradiction by A1, A2, Th29; :: thesis: verum