take {} R ; :: thesis: {} R is clique
let x1, x2 be object ; :: according to RELAT_2:def 6,DILWORTH:def 1 :: thesis: ( not x1 in {} R or not x2 in {} R or x1 = x2 or [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R )
thus ( not x1 in {} R or not x2 in {} R or x1 = x2 or [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R ) ; :: thesis: verum