let S be Subset of R; :: thesis: ( S is trivial implies S is clique )
assume A1: S is trivial ; :: thesis: S is clique
let x1, x2 be object ; :: according to RELAT_2:def 6,DILWORTH:def 1 :: thesis: ( not x1 in S or not x2 in S or x1 = x2 or [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R )
thus ( not x1 in S or not x2 in S or x1 = x2 or [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R ) by A1, ZFMISC_1:def 10; :: thesis: verum