let X be trivial set ; :: thesis: for R being Relation of X st not R is empty holds
ex x being set st R = {[x,x]}
let R be Relation of X; :: thesis: ( not R is empty implies ex x being set st R = {[x,x]} )
assume A1: not R is empty ; :: thesis: ex x being set st R = {[x,x]}
consider x being set such that
A2: x in R by A1, XBOOLE_0:def 1;
consider y, z being set such that
A3: ( x = [y,z] & y in X & z in X ) by A2, RELSET_1:6;
consider a being set such that
A4: X = {a} by A3, REALSET1:def 4;
A5: ( y = a & z = a ) by A3, A4, 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 set ; :: according to TARSKI:def 3 :: thesis: ( not r in R or r in {[a,a]} )
assume A6: r in R ; :: thesis: r in {[a,a]}
consider y, z being set such that
A7: ( r = [y,z] & y in X & z in X ) by A6, RELSET_1:6;
( y = a & z = a ) by A4, A7, TARSKI:def 1;
hence r in {[a,a]} by A7, TARSKI:def 1; :: thesis: verum

end;

let z be set ; :: 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 A2, A3, A5, TARSKI:def 1; :: thesis: verum

end;

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