( rng p c= I & rng q c= I ) by RELAT_1:def 19;
then ( rng (p ^ q) = (rng p) \/ (rng q) & (rng p) \/ (rng q) c= I ) by FINSEQ_1:31, XBOOLE_1:8;
hence rng (p ^ q) c= I ; :: according to RELAT_1:def 19 :: thesis: verum