let L be Lattice; :: thesis: for X, Y, Z being Element of L st X "\/" Y [= Z holds

X [= Z

let X, Y, Z be Element of L; :: thesis: ( X "\/" Y [= Z implies X [= Z )

assume X "\/" Y [= Z ; :: thesis: X [= Z

then X "/\" (X "\/" Y) [= X "/\" Z by LATTICES:9;

then A1: X [= X "/\" Z by LATTICES:def 9;

X "/\" Z [= Z by LATTICES:6;

hence X [= Z by A1, LATTICES:7; :: thesis: verum

X [= Z

let X, Y, Z be Element of L; :: thesis: ( X "\/" Y [= Z implies X [= Z )

assume X "\/" Y [= Z ; :: thesis: X [= Z

then X "/\" (X "\/" Y) [= X "/\" Z by LATTICES:9;

then A1: X [= X "/\" Z by LATTICES:def 9;

X "/\" Z [= Z by LATTICES:6;

hence X [= Z by A1, LATTICES:7; :: thesis: verum