A1:
for x, y, z being Element of (BooleLatt X) holds x "\/" (y "\/" z) = (x "\/" y) "\/" z
by XBOOLE_1:4;

A2: for x, y being Element of (BooleLatt X) holds (x "/\" y) "\/" y = y by XBOOLE_1:22;

A3: 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;

hence BooleLatt X is Lattice-like ; :: thesis: verum

A2: for x, y being Element of (BooleLatt X) holds (x "/\" y) "\/" y = y by XBOOLE_1:22;

A3: 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;

hence BooleLatt X is Lattice-like ; :: thesis: verum