let r be Real; :: according to PARTFUN3:def 1 :: thesis: ( not r in proj2 <*x*> or not r <= 0 )
assume r in rng <*x*> ; :: thesis: not r <= 0
then r in {x} by FINSEQ_1:38;
hence not r <= 0 by TARSKI:def 1; :: thesis: verum