let x be Variable; :: thesis: for M being non empty set holds
( not M |= x 'in' x & M |= 'not' (x 'in' x) )
let M be non empty set ; :: thesis: ( not M |= x 'in' x & M |= 'not' (x 'in' x) )
consider v being Function of VAR ,M;
not M,v |= x 'in' x by Th91;
hence not M |= x 'in' x by ZF_MODEL:def 5; :: thesis: M |= 'not' (x 'in' x)
let v be Function of VAR ,M; :: according to ZF_MODEL:def 5 :: thesis: M,v |= 'not' (x 'in' x)
not M,v |= x 'in' x by Th91;
hence M,v |= 'not' (x 'in' x) by ZF_MODEL:14; :: thesis: verum