theorem Th7: :: OSALG_1:7

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