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

suppose AS: X is empty ; :: thesis: ex b₁ being Relation of X st b₁ is strongly_reflexive

reconsider R = {} as Relation of X,X by RELSET_1:12;
take R ; :: thesis: R is strongly_reflexive
for o being object st o in X holds
[o,o] in R by AS;
hence R is strongly_reflexive by RELAT_2:def 1; :: thesis: verum

end;

suppose AS: not X is empty ; :: thesis: ex b₁ being Relation of X st b₁ is strongly_reflexive

set R = { [x,y] where x, y is Element of X : verum } ;

now :: thesis: for o being object st o in { [x,y] where x, y is Element of X : verum } holds
o in [:X,X:]

let o be object ; :: thesis: ( o in { [x,y] where x, y is Element of X : verum } implies o in [:X,X:] )
assume o in { [x,y] where x, y is Element of X : verum } ; :: thesis: o in [:X,X:]
then consider x, y being Element of X such that
A: o = [x,y] ;
thus o in [:X,X:] by AS, A, ZFMISC_1:def 2; :: thesis: verum

end;

then reconsider R = { [x,y] where x, y is Element of X : verum } as Relation of X by TARSKI:def 3;
take R ; :: thesis: R is strongly_reflexive
for o being object st o in X holds
[o,o] in R ;
hence R is strongly_reflexive by RELAT_2:def 1; :: thesis: verum

end;

end;