let A be non empty non diagonal RelStr ; :: thesis: ex x, y being Element of A st
( x <> y & [x,y] in the InternalRel of A )

now

assume A1: for x, y being Element of A st [x,y] in the InternalRel of A holds
x = y ; :: thesis: ex x, y being Element of A st
( x <> y & [x,y] in the InternalRel of A )
the InternalRel of A c= id the carrier of A

proof

for a, b being set st [a,b] in the InternalRel of A holds
[a,b] in id the carrier of A

proof

let a, b be set ; :: thesis: ( [a,b] in the InternalRel of A implies [a,b] in id the carrier of A )
assume A2: [a,b] in the InternalRel of A ; :: thesis: [a,b] in id the carrier of A
then A3: ( a is Element of A & b is Element of A ) by ZFMISC_1:106;
then a = b by A1, A2;
hence [a,b] in id the carrier of A by A3, RELAT_1:def 10; :: thesis: verum

end;

hence the InternalRel of A c= id the carrier of A by RELAT_1:def 3; :: thesis: verum

end;

hence ex x, y being Element of A st
( x <> y & [x,y] in the InternalRel of A ) by Def1; :: thesis: verum

end;

hence ex x, y being Element of A st
( x <> y & [x,y] in the InternalRel of A ) ; :: thesis: verum