let R be Relation; :: thesis: ( R is symmetric & R is transitive implies R is reflexive )
assume that
A1: R is symmetric and
A2: R is transitive ; :: thesis: R is reflexive
A3: R is_transitive_in field R by A2;
A4: R is_symmetric_in field R by A1;
let a be object ; :: according to RELAT_2:def 1,RELAT_2:def 9 :: thesis: ( a in field R implies [a,a] in R )

A5: now :: thesis: ( a in dom R implies [a,a] in R )

assume a in dom R ; :: thesis: [a,a] in R
then consider b being object such that
A6: [a,b] in R by XTUPLE_0:def 12;
A7: ( a in field R & b in field R ) by A6, RELAT_1:15;
then [b,a] in R by A4, A6;
hence [a,a] in R by A3, A6, A7; :: thesis: verum

end;

now :: thesis: ( a in rng R implies [a,a] in R )

assume a in rng R ; :: thesis: [a,a] in R
then consider b being object such that
A8: [b,a] in R by XTUPLE_0:def 13;
A9: ( a in field R & b in field R ) by A8, RELAT_1:15;
then [a,b] in R by A4, A8;
hence [a,a] in R by A3, A8, A9; :: thesis: verum

end;

hence ( a in field R implies [a,a] in R ) by A5, XBOOLE_0:def 3; :: thesis: verum