let X be set ; :: thesis: for R being Relation of X st R = id X holds
R is total
let R be Relation of X; :: thesis: ( R = id X implies R is total )
assume R = id X ; :: thesis: R is total
hence dom R = X by RELAT_1:71; :: according to PARTFUN1:def 4 :: thesis: verum