thus ( X misses Y implies for w being rational number holds
( not w in X or not w in Y ) ) by XBOOLE_0:3; :: thesis: ( ( for w being rational number holds
( not w in X or not w in Y ) ) implies not X meets Y )
assume A1: for w being rational number holds
( not w in X or not w in Y ) ; :: thesis: not X meets Y
assume X meets Y ; :: thesis: contradiction
then consider x being set such that
A2: ( x in X & x in Y ) by XBOOLE_0:3;
thus contradiction by A1, A2; :: thesis: verum