let R be Relation of X; :: thesis: ( R is strongly_reflexive implies R is reflexive )
assume AS: R is strongly_reflexive ; :: thesis: R is reflexive
H: field R c= X \/ X by RELSET_1:8;

now :: thesis: for o being object st o in field R holds
[o,o] in R

let o be object ; :: thesis: ( o in field R implies [b₁,b₁] in R )
assume A: o in field R ; :: thesis: [b₁,b₁] in R
then reconsider x = o as Element of X by H;

per cases ( X is empty or not X is empty ) ;

suppose X is empty ; :: thesis: [b₁,b₁] in R

hence [o,o] in R by H, A; :: thesis: verum

end;

suppose not X is empty ; :: thesis: [b₁,b₁] in R

then x in X ;
hence [o,o] in R by AS, RELAT_2:def 1; :: thesis: verum

end;

end;

end;

hence R is reflexive by RELAT_2:def 9, RELAT_2:def 1; :: thesis: verum