let R be Relation; :: thesis: ( R is symmetric & R is transitive implies R is reflexive )
assume that
A1: R is_symmetric_in field R and
A2: R is_transitive_in field R ; :: according to RELAT_2:def 11,RELAT_2:def 16 :: thesis: R is reflexive
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 A3: x in field R ; :: thesis: [x,x] in R
then ( x in dom R or x in rng R ) by XBOOLE_0:def 3;
then consider y being object such that
A4: ( [x,y] in R or [y,x] in R ) by XTUPLE_0:def 12, XTUPLE_0:def 13;
( y in rng R or y in dom R ) by A4, XTUPLE_0:def 12, XTUPLE_0:def 13;
then A5: y in field R by XBOOLE_0:def 3;
then ( [x,y] in R & [y,x] in R ) by A1, A3, A4;
hence [x,x] in R by A2, A3, A5; :: thesis: verum