theorem :: YELLOW_1:12

for X being non empty set st ( for x, y being set st x in X & y in X holds
x /\ y in X ) holds
InclPoset X is with_infima