let F be Element of QC-WFF ; :: thesis: for G being Subformula of F holds entry_points_in_subformula_tree G = { t where t is Entry_Point_in_Subformula_Tree of G : t = t }
let G be Subformula of F; :: thesis: entry_points_in_subformula_tree G = { t where t is Entry_Point_in_Subformula_Tree of G : t = t }
thus entry_points_in_subformula_tree G c= { t where t is Entry_Point_in_Subformula_Tree of G : t = t } :: according to XBOOLE_0:def 10 :: thesis: { t where t is Entry_Point_in_Subformula_Tree of G : t = t } c= entry_points_in_subformula_tree G

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in entry_points_in_subformula_tree G or x in { t where t is Entry_Point_in_Subformula_Tree of G : t = t } )
assume x in entry_points_in_subformula_tree G ; :: thesis: x in { t where t is Entry_Point_in_Subformula_Tree of G : t = t }
then x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } by Th49;
then consider t' being Element of dom (tree_of_subformulae F) such that
A1: ( t' = x & (tree_of_subformulae F) . t' = G ) ;
reconsider t' = t' as Entry_Point_in_Subformula_Tree of G by A1, Def5;
t' = t' ;
hence x in { t where t is Entry_Point_in_Subformula_Tree of G : t = t } by A1; :: thesis: verum

end;

thus { t where t is Entry_Point_in_Subformula_Tree of G : t = t } c= entry_points_in_subformula_tree G :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { t where t is Entry_Point_in_Subformula_Tree of G : t = t } or x in entry_points_in_subformula_tree G )
assume x in { t where t is Entry_Point_in_Subformula_Tree of G : t = t } ; :: thesis: x in entry_points_in_subformula_tree G
then consider t being Entry_Point_in_Subformula_Tree of G such that
A2: ( t = x & t = t ) ;
thus x in entry_points_in_subformula_tree G by A2, Th67; :: thesis: verum

end;