set B = BooleLatt {};
let Q be non empty QuantaleStr ; ( LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) = BooleLatt {} implies ( Q is associative & Q is commutative & Q is unital & Q is with_zero & Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like ) )
set a = the Element of Q;
assume A1:
LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) = BooleLatt {}
; ( Q is associative & Q is commutative & Q is unital & Q is with_zero & Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like )
set o = H4(Q);
thus
H4(Q) is associative
MONOID_0:def 12 ( Q is commutative & Q is unital & Q is with_zero & Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like )
A4:
( ( 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;
thus
H4(Q) is commutative
MONOID_0:def 11 ( Q is unital & Q is with_zero & Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like )
thus
H4(Q) is having_a_unity
MONOID_0:def 10 ( Q is with_zero & Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like )
thus
Q is with_zero
( Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like )
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 ) )
; LATTICE3:def 18 ( Q is right-distributive & Q is left-distributive & Q is Lattice-like )
thus
Q is right-distributive
by A2; ( Q is left-distributive & Q is Lattice-like )
thus
Q is left-distributive
by A2; Q is Lattice-like
A7:
( ( for p, q being Element of Q holds (p "/\" q) "\/" q = q ) & ( for p, q being Element of Q holds p "/\" q = q "/\" p ) )
by A2;
( ( 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 ) )
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 A7, A4;
hence
Q is Lattice-like
; verum