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 )

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;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

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

hence
( a in field R implies [a,a] in R )
by A5, XBOOLE_0:def 3; :: thesis: verumassume
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;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