take {} ; :: thesis: rng {} c= X
thus rng {} c= X by XBOOLE_1:2; :: thesis: verum