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