let R be non empty RelStr ; :: thesis: ( R is reflexive implies for w being Element of R holds w in (tau R) . w )

assume aa: R is reflexive ; :: thesis: for w being Element of R holds w in (tau R) . w

let w be Element of R; :: thesis: w in (tau R) . w

[w,w] in the InternalRel of R by aa, LATTAD_1:1;

hence w in (tau R) . w by For3A; :: thesis: verum

assume aa: R is reflexive ; :: thesis: for w being Element of R holds w in (tau R) . w

let w be Element of R; :: thesis: w in (tau R) . w

[w,w] in the InternalRel of R by aa, LATTAD_1:1;

hence w in (tau R) . w by For3A; :: thesis: verum