let x be set ; :: according to VALUED_0:def 12 :: thesis: ( not x in proj1 |.f.| or |.f.| . x is natural )
abs (f . x) is natural ;
hence ( not x in proj1 |.f.| or |.f.| . x is natural ) by Def11; :: thesis: verum