let f be Relation; :: thesis: ( dom f is real-membered iff f is REAL -defined )
thus ( dom f is real-membered implies f is REAL -defined ) :: thesis: ( f is REAL -defined implies dom f is real-membered )

proof

set E = (dom f) \/ REAL;
reconsider X = dom f as Subset of ((dom f) \/ REAL) by XBOOLE_1:7;
reconsider Y = REAL as Subset of ((dom f) \/ REAL) by XBOOLE_1:7;
assume dom f is real-membered ; :: thesis: f is REAL -defined
then for x being Element of (dom f) \/ REAL st x in dom f holds
x in REAL by XREAL_0:def 1;
then X c= Y by SUBSET_1:2;
hence f is REAL -defined by RELAT_1:def 18; :: thesis: verum

end;

thus ( f is REAL -defined implies dom f is real-membered ) ; :: thesis: verum