field R2 = X by ORDERS_1:12;
then A1: R2 is_reflexive_in X by RELAT_2:def 9;
let R be Relation of X; :: thesis: ( R = R1 \, R2 implies ( R is total & R is reflexive ) )
assume A2: R = R1 \, R2 ; :: thesis: ( R is total & R is reflexive )
thus A3: R is total :: thesis: R is reflexive
proof
thus dom R c= X ; :: according to XBOOLE_0:def 10,PARTFUN1:def 2 :: thesis: X c= dom R
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in dom R )
assume A4: x in X ; :: thesis: x in dom R
then reconsider x = x as Element of X ;
[x,x] in R2 by A4, A1;
then ( x,x in R1 or ( not x,x in R1 & x,x in R2 ) ) ;
then x,x in R by A2, Th9;
then [x,x] in R ;
hence x in dom R by XTUPLE_0:def 12; :: thesis: verum
end;
then A5: field R = X by ORDERS_1:12;
let x be object ; :: according to RELAT_2:def 1,RELAT_2:def 9 :: thesis: ( not x in field R or [x,x] in R )
assume A6: x in field R ; :: thesis: [x,x] in R
then reconsider x = x as Element of X by A3, ORDERS_1:12;
[x,x] in R2 by A6, A5, A1;
then ( x,x in R1 or ( not x,x in R1 & x,x in R2 ) ) ;
then x,x in R by A2, Th9;
hence [x,x] in R ; :: thesis: verum