let A be QC-alphabet ; :: thesis: for F being Element of QC-WFF A
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 F be Element of QC-WFF A; :: 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 object ; :: 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 Th19;
then consider t9 being Element of dom (tree_of_subformulae F) such that
A1: t9 = x and
A2: (tree_of_subformulae F) . t9 = G ;
reconsider t9 = t9 as Entry_Point_in_Subformula_Tree of G by A2, Def5;
t9 = t9 ;
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 object ; :: 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 ex t being Entry_Point_in_Subformula_Tree of G st
( t = x & t = t ) ;
hence x in entry_points_in_subformula_tree G by Th35; :: thesis: verum

end;