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

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