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) ;
y c= z by XBOOLE_1:7;
then A1: y <= z by Th3;

A2: now :: thesis: for c being Element of (InclPoset X) st x <= c & y <= c holds
z <= c

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;

x c= z by XBOOLE_1:7;
then x <= z by Th3;
hence x "\/" y = x \/ y by A1, A2, LATTICE3:def 13; :: thesis: verum