thus ( X misses Y implies for i being integer number holds
( not i in X or not i in Y ) ) by XBOOLE_0:3; :: thesis: ( ( for i being integer number holds
( not i in X or not i in Y ) ) implies not X meets Y )
assume A1: for i being integer number holds
( not i in X or not i in Y ) ; :: thesis: not X meets Y
assume X meets Y ; :: thesis: contradiction
then ex x being set st
( x in X & x in Y ) by XBOOLE_0:3;
hence contradiction by A1; :: thesis: verum