let x, y be Variable; :: thesis: Subformulae (x 'in' y) = {(x 'in' y)}

now :: thesis: for a being object holds
( ( a in Subformulae (x 'in' y) implies a in {(x 'in' y)} ) & ( a in {(x 'in' y)} implies a in Subformulae (x 'in' y) ) )

let a be object ; :: thesis: ( ( a in Subformulae (x 'in' y) implies a in {(x 'in' y)} ) & ( a in {(x 'in' y)} implies a in Subformulae (x 'in' y) ) )
thus ( a in Subformulae (x 'in' y) implies a in {(x 'in' y)} ) :: thesis: ( a in {(x 'in' y)} implies a in Subformulae (x 'in' y) )

proof

assume a in Subformulae (x 'in' y) ; :: thesis: a in {(x 'in' y)}
then consider F being ZF-formula such that
A1: F = a and
A2: F is_subformula_of x 'in' y by Def42;
F = x 'in' y by A2, Th77;
hence a in {(x 'in' y)} by A1, TARSKI:def 1; :: thesis: verum

end;

assume a in {(x 'in' y)} ; :: thesis: a in Subformulae (x 'in' y)
then A3: a = x 'in' y by TARSKI:def 1;
x 'in' y is_subformula_of x 'in' y by Th59;
hence a in Subformulae (x 'in' y) by A3, Def42; :: thesis: verum

end;

hence Subformulae (x 'in' y) = {(x 'in' y)} by TARSKI:2; :: thesis: verum