let Q be non empty QuantaleStr ; :: thesis:
set B = BooleLatt {} ;
assume A1: LattStr(# the carrier of Q,the L_join of Q,the L_meet of Q #) = BooleLatt {} ; :: thesis:

A2: now

let x, y be Element of Q; :: thesis:
H₁( BooleLatt {} ) = {{} } by LATTICE3:def 1, ZFMISC_1:1;
then ( x = {} & y = {} ) by A1, TARSKI:def 1;
hence x = y ; :: thesis:

end;

thus H₄(Q) is associative :: according to MONOID_0:def 12 :: thesis:

let a, b, c be Element of Q; :: according to BINOP_1:def 14 :: thesis:
thus H₄(Q) . a,(H₄(Q) . b,c) = H₄(Q) . (H₄(Q) . a,b),c by A2; :: thesis:

end;

thus H₄(Q) is commutative :: according to MONOID_0:def 11 :: thesis:

let a, b be Element of Q; :: according to BINOP_1:def 13 :: thesis:
thus H₄(Q) . a,b = H₄(Q) . b,a by A2; :: thesis:

end;

consider a being Element of Q;
thus H₄(Q) is having_a_unity :: according to MONOID_0:def 10 :: thesis:

take a ; :: according to SETWISEO:def 2 :: thesis:
thus a is_a_left_unity_wrt H₄(Q) :: according to BINOP_1:def 7 :: thesis:

let b be Element of Q; :: according to BINOP_1:def 16 :: thesis:
thus H₄(Q) . a,b = b by A2; :: thesis:

end;

let b be Element of Q; :: according to BINOP_1:def 17 :: thesis:
thus H₄(Q) . b,a = b by A2; :: thesis:

end;

thus Q is with_zero :: thesis:

thus Q is with_left-zero :: according to QUANTAL1:def 4 :: thesis:

take a ; :: according to QUANTAL1:def 2 :: thesis:
thus for b being Element of Q holds a * b = a by A2; :: thesis:

end;

take a ; :: according to QUANTAL1:def 3 :: thesis:
thus for a being Element of Q holds a * a = a by A2; :: thesis:

end;

now

let X be set ; :: thesis:
consider p being Element of (BooleLatt {} ) such that
A3: ( X is_less_than p & ( for r being Element of (BooleLatt {} ) st X is_less_than r holds
p [= r ) ) by LATTICE3:def 18;
reconsider p' = p as Element of Q by A1;
take p' = p'; :: thesis:
thus X is_less_than p' by A1, A3, Th2; :: thesis:
let r' be Element of Q; :: thesis:
reconsider r = r' as Element of (BooleLatt {} ) by A1;
assume X is_less_than r' ; :: thesis:
then X is_less_than r by A1, Th2;
then p [= r by A3;
hence p' [= r' by A1, Th1; :: thesis:

end;

hence for X being set ex p being Element of Q st
( X is_less_than p & ( for r being Element of Q st X is_less_than r holds
p [= r ) ) ; :: according to LATTICE3:def 18 :: thesis:
thus Q is right-distributive :: thesis:

let a be Element of Q; :: according to QUANTAL1:def 5 :: thesis:
let X be set ; :: thesis:
thus a [*] ("\/" X,Q) = "\/" { (a [*] b) where b is Element of Q : b in X } ,Q by A2; :: thesis:

end;

thus Q is left-distributive :: thesis:

let a be Element of Q; :: according to QUANTAL1:def 6 :: thesis:
let X be set ; :: thesis:
thus ("\/" X,Q) [*] a = "\/" { (b [*] a) where b is Element of Q : b in X } ,Q by A2; :: thesis:

end;

( ( for p, q being Element of Q holds p "\/" q = q "\/" p ) & ( for p, q, r being Element of Q holds p "\/" (q "\/" r) = (p "\/" q) "\/" r ) & ( for p, q being Element of Q holds (p "/\" q) "\/" q = q ) & ( for p, q being Element of Q holds p "/\" q = q "/\" p ) & ( for p, q, r being Element of Q holds p "/\" (q "/\" r) = (p "/\" q) "/\" r ) & ( for p, q being Element of Q holds p "/\" (p "\/" q) = p ) ) by A2;
then ( Q is join-commutative & Q is join-associative & Q is meet-absorbing & Q is meet-commutative & Q is meet-associative & Q is join-absorbing ) by LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
hence Q is Lattice-like ; :: thesis: