set R = CompleteRelStr n;
set iR = the InternalRel of (CompleteRelStr n);
let x, y be object ; RELAT_2:def 6,DILWORTH:def 1 ( not x in [#] (CompleteRelStr n) or not y in [#] (CompleteRelStr n) or x = y or [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) )
assume
( x in [#] (CompleteRelStr n) & y in [#] (CompleteRelStr n) )
; ( x = y or [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) )
then A1:
( x in n & y in n )
by Def7;
assume
x <> y
; ( [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) )
hence
( [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) )
by A1, Th32; verum