theorem Th8: :: YELLOW_1:8

for X being non empty set
for x, y being Element of (InclPoset X) st x \/ y in X holds
x "\/" y = x \/ y