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;

now

let a be set ; :: thesis: ( a in field R implies [a,a] in R )

A5: now

assume a in dom R ; :: thesis: [a,a] in R
then consider b being set such that
A6: [a,b] in R by RELAT_1:def 4;
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;

A8: now

assume a in rng R ; :: thesis: [a,a] in R
then consider b being set such that
A9: [b,a] in R by RELAT_1:def 5;
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;

assume a in field R ; :: thesis: [a,a] in R
then a in (dom R) \/ (rng R) by RELAT_1:def 6;
hence [a,a] in R by A5, A8, XBOOLE_0:def 3; :: thesis: verum

end;

then R is_reflexive_in field R by Def1;
hence R is reflexive by Def9; :: thesis: verum