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) )
set v = the Function of VAR,M;
not M, the Function of VAR,M |= x 'in' x by Th80;
hence not M |= x 'in' x ; :: 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 Th80;
hence M,v |= 'not' (x 'in' x) by ZF_MODEL:14; :: thesis: verum