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 set ; :: 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 set such that
A4: ( [x,y] in R or [y,x] in R ) by RELAT_1:def 4, RELAT_1:def 5;
( y in rng R or y in dom R ) by A4, RELAT_1:def 4, RELAT_1:def 5;
then A5: y in field R by XBOOLE_0:def 3;
then ( [x,y] in R & [y,x] in R ) by A1, A3, A4, RELAT_2:def 3;
hence [x,x] in R by A2, A3, A5, RELAT_2:def 8; :: thesis: verum