let X be set ; :: thesis: for R being Relation of X holds field R c= X
let R be Relation of X; :: thesis: field R c= X
( dom R c= X & rng R c= X ) ;
hence field R c= X by XBOOLE_1:8; :: thesis: verum