let F, G be Element of QC-WFF ; :: thesis: F -entry_points_in_subformula_tree_of G = { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G }
thus F -entry_points_in_subformula_tree_of G c= { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } :: according to XBOOLE_0:def 10 :: thesis: { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } c= F -entry_points_in_subformula_tree_of G

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F -entry_points_in_subformula_tree_of G or x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } )
assume A1: x in F -entry_points_in_subformula_tree_of G ; :: thesis: x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G }
F -entry_points_in_subformula_tree_of G c= dom (tree_of_subformulae F) by TREES_1:def 14;
then reconsider t' = x as Element of dom (tree_of_subformulae F) by A1;
(tree_of_subformulae F) . t' = G by A1, Def3;
hence x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } ; :: thesis: verum

end;

thus { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } c= F -entry_points_in_subformula_tree_of G :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } or x in F -entry_points_in_subformula_tree_of G )
assume x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } ; :: thesis: x in F -entry_points_in_subformula_tree_of G
then consider t' being Element of dom (tree_of_subformulae F) such that
A2: ( t' = x & (tree_of_subformulae F) . t' = G ) ;
thus x in F -entry_points_in_subformula_tree_of G by A2, Def3; :: thesis: verum

end;