let X, Y be set ; :: thesis: ( ( for x being set st x in X holds
not x in Y ) iff X misses Y )
thus ( ( for x being set st x in X holds
not x in Y ) implies X misses Y ) :: thesis: ( X misses Y implies for x being set st x in X holds
not x in Y )

proof

assume A1: for x being set st x in X holds
not x in Y ; :: thesis: X misses Y

now

given x1 being set such that A2: x1 in X /\ Y ; :: thesis: contradiction
A3: x1 in X by A2, XBOOLE_0:def 4;
x1 in Y by A2, XBOOLE_0:def 4;
hence contradiction by A1, A3; :: thesis: verum

end;

then X /\ Y = {} by XBOOLE_0:def 1;
hence X misses Y by XBOOLE_0:def 7; :: thesis: verum

end;

assume A4: X misses Y ; :: thesis: for x being set st x in X holds
not x in Y

now

let x be set ; :: thesis: ( x in X implies not x in Y )
assume A5: x in X ; :: thesis: not x in Y

now

assume x in Y ; :: thesis: contradiction
then x in X /\ Y by A5, XBOOLE_0:def 4;
hence contradiction by A4, XBOOLE_0:def 7; :: thesis: verum

end;

hence not x in Y ; :: thesis: verum

end;

hence for x being set st x in X holds
not x in Y ; :: thesis: verum