let x be Variable; :: thesis: for M being non empty set
for v being Function of VAR,M holds not M,v |= x 'in' x
let M be non empty set ; :: thesis: for v being Function of VAR,M holds not M,v |= x 'in' x
let v be Function of VAR,M; :: thesis: not M,v |= x 'in' x
not v . x in v . x ;
hence not M,v |= x 'in' x by ZF_MODEL:13; :: thesis: verum