let p be Element of CQC-WFF ; :: thesis: for x, y being bound_QC-variable holds QuantNbr p = QuantNbr (p . (x,y))
let x, y be bound_QC-variable; :: thesis: QuantNbr p = QuantNbr (p . (x,y))
QuantNbr p = QuantNbr (CQC_Sub [p,(Sbst (x,y))]) by SUBSTUT2:25;
hence QuantNbr p = QuantNbr (p . (x,y)) by SUBSTUT2:def 1; :: thesis: verum