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

set v = the Function of VAR,M;
assume that
A1: for v being Function of VAR,M holds M,v |= 'not' (x 'in' y) and
A2: 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 )
set a = the Element of X /\ M;
assume X in M ; :: thesis: X misses M
then reconsider m = X as Element of M ;
assume A3: X /\ M <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then reconsider a = the Element of X /\ M as Element of M by XBOOLE_0:def 4;
M,( the Function of VAR,M / (x,a)) / (y,m) |= 'not' (x 'in' y) by A1;
then not M,( the Function of VAR,M / (x,a)) / (y,m) |= x 'in' y by ZF_MODEL:14;
then A4: not (( the Function of VAR,M / (x,a)) / (y,m)) . x in (( the Function of VAR,M / (x,a)) / (y,m)) . y by ZF_MODEL:13;
A5: ( ( the Function of VAR,M / (x,a)) . x = a & (( the Function of VAR,M / (x,a)) / (y,m)) . y = m ) by FUNCT_7:128;
(( the Function of VAR,M / (x,a)) / (y,m)) . x = ( the Function of VAR,M / (x,a)) . x by A2, FUNCT_7:32;
hence contradiction by A3, A4, A5, XBOOLE_0:def 4; :: thesis: verum

end;

now :: thesis: ( ( for X being set st X in M holds
X misses M ) implies for v being Function of VAR,M holds M,v |= 'not' (x 'in' y) )

assume A6: 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 A6;
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 Th81; :: thesis: verum