let P be a_partition of the carrier of R; :: thesis: ( P is empty implies P is Clique-wise )
assume P is empty ; :: thesis: P is Clique-wise
let x be set ; :: according to DILWORTH:def 11 :: thesis: ( x in P implies x is Clique of R )
thus ( x in P implies x is Clique of R ) ; :: thesis: verum