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