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
y <= x "\/" y by A1, YELLOW_0:22;
then A2: y c= x "\/" y by Th3;
x <= x "\/" y by A1, YELLOW_0:22;
then x c= x "\/" y by Th3;
hence x \/ y c= x "\/" y by A2, XBOOLE_1:8; :: thesis: verum