let L be B_Lattice; :: thesis: for X, Y, Z being Element of L st X [= Y "\/" Z & X "/\" Z = Bottom L holds
X [= Y
let X, Y, Z be Element of L; :: thesis: ( X [= Y "\/" Z & X "/\" Z = Bottom L implies X [= Y )
assume that
A1: X [= Y "\/" Z and
A2: X "/\" Z = Bottom L ; :: thesis: X [= Y
X "/\" (Y "\/" Z) = X by A1, LATTICES:4;
then (X "/\" Y) "\/" (Bottom L) = X by A2, LATTICES:def 11;
hence X [= Y by LATTICES:4; :: thesis: verum