assume {} in rng (p ^ q) ; :: according to RELAT_1:def 9 :: thesis: contradiction
then {} in (rng p) \/ (rng q) by FINSEQ_1:44;
then ( {} in rng p or {} in rng q ) by XBOOLE_0:def 3;
hence contradiction by RELAT_1:def 9; :: thesis: verum