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