let n be Element of NAT ; :: thesis: VERUM <> prop n
assume A1: not VERUM <> prop n ; :: thesis: contradiction
VERUM . 1 = 0 by FINSEQ_1:40;
hence contradiction by A1, FINSEQ_1:40; :: thesis: verum