set R = CompleteRelStr n;
set iR = the InternalRel of (CompleteRelStr n);
let x, y be object ; :: according to RELAT_2:def 6,DILWORTH:def 1 :: thesis: ( 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) ) ; :: thesis: ( 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 ; :: thesis: ( [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; :: thesis: verum