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, Def16;
A4: R is_symmetric_in field R by A1, Def11;
let a be set ; :: 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 set 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, Def3;
hence [a,a] in R by A3, A6, A7, Def8; :: 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 set such that
A9: [b,a] in R by XTUPLE_0:def 13;
A10: ( a in field R & b in field R ) by A9, RELAT_1:15;
then [a,b] in R by A4, A9, Def3;
hence [a,a] in R by A3, A9, A10, Def8; :: thesis: verum

end;

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