theorem :: DILWORTH:13

for R being non empty RelStr
for a1, a2 being Element of R st a1 <> a2 & {a1,a2} is StableSet of R holds
( not a1 <= a2 & not a2 <= a1 )