let A be QC-alphabet ; :: thesis: for F, G being Element of QC-WFF A holds 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 }
let F, G be Element of QC-WFF A; :: 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 object ; :: 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 11;
then reconsider t9 = x as Element of dom (tree_of_subformulae F) by A1;
(tree_of_subformulae F) . t9 = 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 object ; :: 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 ex t9 being Element of dom (tree_of_subformulae F) st
( t9 = x & (tree_of_subformulae F) . t9 = G ) ;
hence x in F -entry_points_in_subformula_tree_of G by Def3; :: thesis: verum

end;