theorem Th9: :: YELLOW_1:9

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