let x, y be Variable; :: thesis: Subformulae (x '=' y) = {(x '=' y)}
now :: thesis: for a being object holds
( ( a in Subformulae (x '=' y) implies a in {(x '=' y)} ) & ( a in {(x '=' y)} implies a in Subformulae (x '=' y) ) )
let a be object ; :: thesis: ( ( a in Subformulae (x '=' y) implies a in {(x '=' y)} ) & ( a in {(x '=' y)} implies a in Subformulae (x '=' y) ) )
thus ( a in Subformulae (x '=' y) implies a in {(x '=' y)} ) :: thesis: ( a in {(x '=' y)} implies a in Subformulae (x '=' y) )
proof
assume a in Subformulae (x '=' y) ; :: thesis: a in {(x '=' y)}
then consider F being ZF-formula such that
A1: F = a and
A2: F is_subformula_of x '=' y by Def42;
F = x '=' y by A2, Th76;
hence a in {(x '=' y)} by A1, TARSKI:def 1; :: thesis: verum
end;
assume a in {(x '=' y)} ; :: thesis: a in Subformulae (x '=' y)
then A3: a = x '=' y by TARSKI:def 1;
x '=' y is_subformula_of x '=' y by Th59;
hence a in Subformulae (x '=' y) by A3, Def42; :: thesis: verum
end;
hence Subformulae (x '=' y) = {(x '=' y)} by TARSKI:2; :: thesis: verum