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