theorem Ble1: :: LATTAD_1:1

for L being non empty 1-sorted
for R being total Relation of the carrier of L holds
( R is reflexive iff for x being Element of L holds [x,x] in R )