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

assume R in rng (X --> L) ; :: thesis: not R is empty

hence not R is empty by TARSKI:def 1; :: thesis: verum