theorem Th8: :: DILWORTH:8

for R being non empty RelStr
for a1, a2 being Element of R st ( a1 <= a2 or a2 <= a1 ) holds
{a1,a2} is Clique of R