let A be QC-alphabet ; :: thesis: for F, G, H being Element of QC-WFF A holds { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G) : ( t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H ) } c= F -entry_points_in_subformula_tree_of H
let F, G, H be Element of QC-WFF A; :: thesis: { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G) : ( t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H ) } c= F -entry_points_in_subformula_tree_of H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G) : ( t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H ) } or x in F -entry_points_in_subformula_tree_of H )
assume x in { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G) : ( t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H ) } ; :: thesis: x in F -entry_points_in_subformula_tree_of H
then ex t being Element of dom (tree_of_subformulae F) ex s being Element of dom (tree_of_subformulae G) st
( x = t ^ s & t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H ) ;
hence x in F -entry_points_in_subformula_tree_of H by Th27; :: thesis: verum