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