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