let Al be QC-alphabet ; :: thesis: for x, y being bound_QC-variable of Al holds (VERUM Al) . (x,y) = VERUM Al
let x, y be bound_QC-variable of Al; :: thesis: (VERUM Al) . (x,y) = VERUM Al
set S = [(VERUM Al),(Sbst (x,y))];
[(VERUM Al),(Sbst (x,y))] is Al -Sub_VERUM by SUBSTUT1:def 19;
hence (VERUM Al) . (x,y) = VERUM Al by SUBLEMMA:3; :: thesis: verum