per cases ( X is empty or not X is empty ) ;
suppose AS: X is empty ; :: thesis: ex b1 being Relation of X st b1 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 b1 being Relation of X st b1 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;