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 :: thesis: ( ( for x, y being Element of A st [x,y] in the InternalRel of A holds
x = y ) implies ex x, y being Element of A st
( x <> y & [x,y] in the InternalRel of A ) )

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 )
for a, b being object st [a,b] in the InternalRel of A holds
[a,b] in id the carrier of A

proof

let a, b be object ; :: 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 by ZFMISC_1:87;
b is Element of A by A2, ZFMISC_1:87;
then a = b by A1, A2, A3;
hence [a,b] in id the carrier of A by A3, RELAT_1:def 10; :: thesis: verum

end;

then the InternalRel of A c= id the carrier of A by RELAT_1:def 3;
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