let x, y be Variable; :: thesis: for M being non empty set holds
( M |= 'not' (x 'in' y) iff ( x = y or for X being set st X in M holds
X misses M ) )
let M be non empty set ; :: thesis: ( M |= 'not' (x 'in' y) iff ( x = y or for X being set st X in M holds
X misses M ) )
thus ( not M |= 'not' (x 'in' y) or x = y or for X being set st X in M holds
X misses M ) :: thesis: ( ( x = y or for X being set st X in M holds
X misses M ) implies M |= 'not' (x 'in' y) )

proof

assume A1: ( ( for v being Function of VAR ,M holds M,v |= 'not' (x 'in' y) ) & x <> y ) ; :: according to ZF_MODEL:def 5 :: thesis: for X being set st X in M holds
X misses M
let X be set ; :: thesis: ( X in M implies X misses M )
assume X in M ; :: thesis: X misses M
then reconsider m = X as Element of M ;
assume A2: X /\ M <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
consider a being Element of X /\ M;
reconsider a = a as Element of M by A2, XBOOLE_0:def 4;
consider v being Function of VAR ,M;
M,(v / x,a) / y,m |= 'not' (x 'in' y) by A1;
then not M,(v / x,a) / y,m |= x 'in' y by ZF_MODEL:14;
then ( not ((v / x,a) / y,m) . x in ((v / x,a) / y,m) . y & (v / x,a) . x = a & ((v / x,a) / y,m) . y = m & ((v / x,a) / y,m) . x = (v / x,a) . x ) by A1, FUNCT_7:34, FUNCT_7:130, ZF_MODEL:13;
hence contradiction by A2, XBOOLE_0:def 4; :: thesis: verum

end;

now

assume A3: for X being set st X in M holds
X misses M ; :: thesis: for v being Function of VAR ,M holds M,v |= 'not' (x 'in' y)
let v be Function of VAR ,M; :: thesis: M,v |= 'not' (x 'in' y)
v . y misses M by A3;
then not v . x in v . y by XBOOLE_0:3;
then not M,v |= x 'in' y by ZF_MODEL:13;
hence M,v |= 'not' (x 'in' y) by ZF_MODEL:14; :: thesis: verum

end;

hence ( ( x = y or for X being set st X in M holds
X misses M ) implies M |= 'not' (x 'in' y) ) by Th92, ZF_MODEL:def 5; :: thesis: verum