theorem Th6: :: OSALG_1:6

for S being non empty Poset
for w1, w2 being Element of the carrier of S * st w1 <= w2 & w2 <= w1 holds
w1 = w2