thus ( X misses Y implies for N being ExtNat holds
( not N in X or not N in Y ) ) by XBOOLE_0:3; :: thesis: ( ( for N being ExtNat holds
( not N in X or not N in Y ) ) implies X misses Y )
assume for N being ExtNat holds
( not N in X or not N in Y ) ; :: thesis: X misses Y
then for x being object holds
( not x in X or not x in Y ) ;
hence X misses Y by XBOOLE_0:3; :: thesis: verum