let x, y be Element of (BoolePoset X); :: according to YELLOW_6:def 3 :: thesis: ex z being Element of (BoolePoset X) st
( x <= z & y <= z )
take x "\/" y ; :: thesis: ( x <= x "\/" y & y <= x "\/" y )
A1: y c= x \/ y by XBOOLE_1:7;
( x "\/" y = x \/ y & x c= x \/ y ) by XBOOLE_1:7, YELLOW_1:17;
hence ( x <= x "\/" y & y <= x "\/" y ) by A1, YELLOW_1:2; :: thesis: verum