let n be Nat; :: thesis: for x, y being set st x in n & y in n holds
( [x,y] in the InternalRel of (CompleteRelStr n) iff x <> y )
let x, y be set ; :: thesis: ( x in n & y in n implies ( [x,y] in the InternalRel of (CompleteRelStr n) iff x <> y ) )
assume A1: ( x in n & y in n ) ; :: thesis: ( [x,y] in the InternalRel of (CompleteRelStr n) iff x <> y )
hereby :: thesis: ( x <> y implies [x,y] in the InternalRel of (CompleteRelStr n) )
assume [x,y] in the InternalRel of (CompleteRelStr n) ; :: thesis: x <> y
then [x,y] in [:n,n:] \ (id n) by Def8;
then not [x,y] in id n by XBOOLE_0:def 5;
hence x <> y by A1, RELAT_1:def 10; :: thesis: verum
end;
assume x <> y ; :: thesis: [x,y] in the InternalRel of (CompleteRelStr n)
then ( [x,y] in [:n,n:] & not [x,y] in id n ) by A1, RELAT_1:def 10, ZFMISC_1:87;
then [x,y] in [:n,n:] \ (id n) by XBOOLE_0:def 5;
hence [x,y] in the InternalRel of (CompleteRelStr n) by Def8; :: thesis: verum