A1: for x, y being Element of (BooleLatt X) holds x "\/" y = y "\/" x ;
A2: for x, y, z being Element of (BooleLatt X) holds x "\/" (y "\/" z) = (x "\/" y) "\/" z by XBOOLE_1:4;
A3: for x, y being Element of (BooleLatt X) holds (x "/\" y) "\/" y = y by XBOOLE_1:22;
A4: for x, y being Element of (BooleLatt X) holds x "/\" y = y "/\" x ;
A5: for x, y, z being Element of (BooleLatt X) holds x "/\" (y "/\" z) = (x "/\" y) "/\" z by XBOOLE_1:16;
for x, y being Element of (BooleLatt X) holds x "/\" (x "\/" y) = x by XBOOLE_1:21;
then ( BooleLatt X is join-commutative & BooleLatt X is join-associative & BooleLatt X is meet-absorbing & BooleLatt X is meet-commutative & BooleLatt X is meet-associative & BooleLatt X is join-absorbing ) by A1, A2, A3, A4, A5, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
hence BooleLatt X is Lattice-like ; :: thesis: verum