let A be QC-alphabet ; :: thesis: for F being Element of QC-WFF A holds rng (tree_of_subformulae F) = Subformulae F
let F be Element of QC-WFF A; :: thesis: rng (tree_of_subformulae F) = Subformulae F
thus rng (tree_of_subformulae F) c= Subformulae F :: according to XBOOLE_0:def 10 :: thesis: Subformulae F c= rng (tree_of_subformulae F)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (tree_of_subformulae F) or y in Subformulae F )
assume A1: y in rng (tree_of_subformulae F) ; :: thesis: y in Subformulae F
then y is Element of QC-WFF A by RELAT_1:167;
then consider G being Element of QC-WFF A such that
A2: G = y ;
G is_subformula_of F by A1, A2, Th10;
hence y in Subformulae F by A2, QC_LANG2:def 22; :: thesis: verum

end;

thus Subformulae F c= rng (tree_of_subformulae F) :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Subformulae F or y in rng (tree_of_subformulae F) )
assume y in Subformulae F ; :: thesis: y in rng (tree_of_subformulae F)
then ex G being Element of QC-WFF A st
( G = y & G is_subformula_of F ) by QC_LANG2:def 22;
hence y in rng (tree_of_subformulae F) by Th10; :: thesis: verum

end;