let p be MP-variable; :: thesis: VERUM <> @ p
assume A1: not VERUM <> @ p ; :: thesis: contradiction
( rng (@ p) = {p} & rng VERUM = {[0,0]} ) by FUNCOP_1:8;
then [0,0] in {p} by A1, TARSKI:def 1;
hence contradiction by Lm5, Th21, XBOOLE_0:3; :: thesis: verum