let X, Y be set ; :: thesis: for R being Relation of X,Y holds field R c= X \/ Y
let R be Relation of X,Y; :: thesis: field R c= X \/ Y
(dom R) \/ (rng R) c= X \/ Y by XBOOLE_1:13;
hence field R c= X \/ Y ; :: thesis: verum