let X be set ; :: thesis: for R being Relation of X holds
( ( R is total & R is reflexive ) iff id X c= R )
let R be Relation of X; :: thesis: ( ( R is total & R is reflexive ) iff id X c= R )

hereby :: thesis: ( id X c= R implies ( R is total & R is reflexive ) )

assume ( R is total & R is reflexive ) ; :: thesis: id X c= R
then A1: ( dom R = X & id (field R) c= R ) by PARTFUN1:def 2, RELAT_2:1;
then field R = X \/ (rng R) by RELAT_1:def 6;
hence id X c= R by A1, XBOOLE_1:12; :: thesis: verum

end;

assume A2: id X c= R ; :: thesis: ( R is total & R is reflexive )
field R c= X \/ X by RELSET_1:8;
then id (field R) c= id X by FUNCT_4:3;
then A3: id (field R) c= R by A2;
dom (id X) c= dom R by A2, RELAT_1:11;
hence ( R is total & R is reflexive ) by A3, XBOOLE_0:def 10, RELAT_2:1, PARTFUN1:def 2; :: thesis: verum