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]}

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

hence
ex x being object st R = {[x,x]}
; :: thesis: verum
thus
R c= {[a,a]}
:: according to XBOOLE_0:def 10 :: thesis: {[a,a]} c= R

assume z in {[a,a]} ; :: thesis: z in R

hence z in R by A1, A2, A6, TARSKI:def 1; :: thesis: verum

end;proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {[a,a]} or z in R )
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;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

assume z in {[a,a]} ; :: thesis: z in R

hence z in R by A1, A2, A6, TARSKI:def 1; :: thesis: verum