let X be non empty set ; :: thesis: for R being total Relation of X
for S being Relation of X holds R \/ S is total
let R be total Relation of X; :: thesis: for S being Relation of X holds R \/ S is total
let S be Relation of X; :: thesis: R \/ S is total
A1: dom R = X by PARTFUN1:def 2;
dom (R \/ S) = X \/ (dom S) by A1, XTUPLE_0:23;
hence R \/ S is total by PARTFUN1:def 2, XBOOLE_1:12; :: thesis: verum