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