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 ;
consider a being object such that
A5: X = {a} by ;
A6: ( y = a & z = a ) by ;
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 ;
hence r in {[a,a]} by ; :: 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 ; :: thesis: verum
end;
hence ex x being object st R = {[x,x]} ; :: thesis: verum