let s be 1-sorted ; :: according to WAYBEL_3:def 7 :: thesis: ( not s in rng (I --> S) or not s is empty )
assume s in rng (I --> S) ; :: thesis: not s is empty
hence not s is empty by TARSKI:def 1; :: thesis: verum