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

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