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