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

now

let a be set ; :: 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 & F is_subformula_of x 'in' y ) by Def42;
F = x 'in' y by A1, Th98;
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 ( a = x 'in' y & x 'in' y is_subformula_of x 'in' y ) by Th79, TARSKI:def 1;
hence a in Subformulae (x 'in' y) by Def42; :: thesis: verum

end;

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