let R be Relation of X; :: thesis: ( R is strongly_reflexive implies not R is empty )
assume AS: R is strongly_reflexive ; :: thesis: not R is empty
set x = the Element of X;
[ the Element of X, the Element of X] in R by AS, RELAT_2:def 1;
hence not R is empty ; :: thesis: verum