let X be non empty set ; :: thesis: for x, y being Element of (InclPoset X) st x \/ y in X holds
x "\/" y = x \/ y
let x, y be Element of (InclPoset X); :: thesis: ( x \/ y in X implies x "\/" y = x \/ y )
assume x \/ y in X ; :: thesis: x "\/" y = x \/ y
then reconsider z = x \/ y as Element of (InclPoset X) ;
( x c= z & y c= z ) by XBOOLE_1:7;
then A1: ( x <= z & y <= z ) by Th3;

now

let c be Element of (InclPoset X); :: thesis: ( x <= c & y <= c implies z <= c )
assume ( x <= c & y <= c ) ; :: thesis: z <= c
then ( x c= c & y c= c ) by Th3;
then z c= c by XBOOLE_1:8;
hence z <= c by Th3; :: thesis: verum

end;

hence x "\/" y = x \/ y by A1, LATTICE3:def 13; :: thesis: verum