let X be trivial set ; :: thesis: for R being Relation of X st not R is empty holds
ex x being object st R = {[x,x]}
let R be Relation of X; :: thesis: ( not R is empty implies ex x being object st R = {[x,x]} )
assume not R is empty ; :: thesis: ex x being object st R = {[x,x]}
then consider x being object such that
A1: x in R ;
consider y, z being object such that
A2: x = [y,z] and
A3: y in X and
A4: z in X by A1, RELSET_1:2;
consider a being object such that
A5: X = {a} by A3, ZFMISC_1:131;
A6: ( y = a & z = a ) by A3, A4, A5, TARSKI:def 1;
R = {[a,a]}

proof

thus R c= {[a,a]} :: according to XBOOLE_0:def 10 :: thesis: {[a,a]} c= R

proof

let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in R or r in {[a,a]} )
assume r in R ; :: thesis: r in {[a,a]}
then consider y, z being object such that
A7: r = [y,z] and
A8: ( y in X & z in X ) by RELSET_1:2;
( y = a & z = a ) by A5, A8, TARSKI:def 1;
hence r in {[a,a]} by A7, TARSKI:def 1; :: thesis: verum

end;

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {[a,a]} or z in R )
assume z in {[a,a]} ; :: thesis: z in R
hence z in R by A1, A2, A6, TARSKI:def 1; :: thesis: verum

end;

hence ex x being object st R = {[x,x]} ; :: thesis: verum