let x, y be Variable; :: thesis: for F being ZF-formula holds not F is_proper_subformula_of x '=' y
let F be ZF-formula; :: thesis: not F is_proper_subformula_of x '=' y
assume F is_proper_subformula_of x '=' y ; :: thesis: contradiction
then ex G being ZF-formula st G is_immediate_constituent_of x '=' y by Th63;
hence contradiction by Th50; :: thesis: verum