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 = tree_of_subformulae 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 = tree_of_subformulae 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 = tree_of_subformulae G } :: according to XBOOLE_0:def 10 :: thesis: { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) | t = tree_of_subformulae 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 = tree_of_subformulae 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 = tree_of_subformulae 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 = tree_of_subformulae G by A1, Th31;
hence x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) | t = tree_of_subformulae G } ; :: thesis: verum
end;
thus { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) | t = tree_of_subformulae 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 = tree_of_subformulae 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 = tree_of_subformulae 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 = tree_of_subformulae G ) ;
hence x in F -entry_points_in_subformula_tree_of G by Th31; :: thesis: verum
end;