let X be non empty set ; :: thesis: ( InclPoset X is with_suprema implies for x, y being Element of (InclPoset X) holds x \/ y c= x "\/" y )
assume A1: InclPoset X is with_suprema ; :: thesis: for x, y being Element of (InclPoset X) holds x \/ y c= x "\/" y
let x, y be Element of (InclPoset X); :: thesis: x \/ y c= x "\/" y
( x <= x "\/" y & y <= x "\/" y ) by A1, YELLOW_0:22;
then ( x c= x "\/" y & y c= x "\/" y ) by Th3;
hence x \/ y c= x "\/" y by XBOOLE_1:8; :: thesis: verum