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