let X be non empty set ; :: thesis: for R being total reflexive Relation of X holds R /\ (R ~) is total
let R be total reflexive Relation of X; :: thesis: R /\ (R ~) is total
A4: field R = X by FieldTot;
then A5: field (R ~) = X by RELAT_1:21;
A6: id X c= R by A4, RELAT_2:1;
id (field (R ~)) c= R ~ by RELAT_2:1;
then id X c= R /\ (R ~) by XBOOLE_1:19, A6, A5;
then dom (id X) c= dom (R /\ (R ~)) by RELAT_1:11;
hence R /\ (R ~) is total by PARTFUN1:def 2, XBOOLE_0:def 10; :: thesis: verum