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

proof

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

end;

thus ( f is INT -defined implies dom f is integer-membered ) ; :: thesis: verum