let L be GAD_Lattice; :: thesis: for x, y being Element of L st y [= x "\/" y holds
ex z being Element of L st
( x [= z & y [= z )
let x, y be Element of L; :: thesis: ( y [= x "\/" y implies ex z being Element of L st
( x [= z & y [= z ) )
assume A1: y [= x "\/" y ; :: thesis: ex z being Element of L st
( x [= z & y [= z )
take z = x "\/" y; :: thesis: ( x [= z & y [= z )
thus ( x [= z & y [= z ) by LemX3, A1; :: thesis: verum