let A be QC-alphabet ; :: thesis: for F, H being Element of QC-WFF A
for x being bound_QC-variable of A st All (x,H) is_subformula_of F holds
H is_proper_subformula_of F
let F, H be Element of QC-WFF A; :: thesis: for x being bound_QC-variable of A st All (x,H) is_subformula_of F holds
H is_proper_subformula_of F
let x be bound_QC-variable of A; :: thesis: ( All (x,H) is_subformula_of F implies H is_proper_subformula_of F )
H is_proper_subformula_of All (x,H) by Th71;
hence ( All (x,H) is_subformula_of F implies H is_proper_subformula_of F ) by Th63; :: thesis: verum