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