set B = BooleLatt {};

let Q be non empty QuantaleStr ; :: thesis: ( 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 {} ; :: thesis: ( 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 )

_{4}(Q);

thus H_{4}(Q) is associative
:: according to MONOID_0:def 12 :: thesis: ( 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 )

thus H_{4}(Q) is commutative
:: according to MONOID_0:def 11 :: thesis: ( Q is unital & Q is with_zero & Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like )_{4}(Q) is having_a_unity
:: according to MONOID_0:def 10 :: thesis: ( Q is with_zero & Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like )

( 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: ( Q is right-distributive & Q is left-distributive & Q is Lattice-like )

thus Q is right-distributive by A2; :: thesis: ( Q is left-distributive & Q is Lattice-like )

thus Q is left-distributive by A2; :: thesis: 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 ; :: thesis: verum

let Q be non empty QuantaleStr ; :: thesis: ( 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 {} ; :: thesis: ( 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 )

A2: now :: thesis: for x, y being Element of Q holds x = y

set o = Hlet x, y be Element of Q; :: thesis: x = y

A3: H_{1}( BooleLatt {}) = {{}}
by LATTICE3:def 1, ZFMISC_1:1;

then x = {} by A1, TARSKI:def 1;

hence x = y by A1, A3, TARSKI:def 1; :: thesis: verum

end;A3: H

then x = {} by A1, TARSKI:def 1;

hence x = y by A1, A3, TARSKI:def 1; :: thesis: verum

thus H

proof

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
for a, b, c being Element of Q holds H_{4}(Q) . (a,(H_{4}(Q) . (b,c))) = H_{4}(Q) . ((H_{4}(Q) . (a,b)),c)
by A2; :: according to BINOP_1:def 3 :: thesis: verum

end;thus H

proof

thus
H
thus
for a, b being Element of Q holds H_{4}(Q) . (a,b) = H_{4}(Q) . (b,a)
by A2; :: according to BINOP_1:def 2 :: thesis: verum

end;proof

thus
Q is with_zero
:: thesis: ( Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like )
take
the Element of Q
; :: according to SETWISEO:def 2 :: thesis: the Element of Q is_a_unity_wrt H_{4}(Q)

thus the Element of Q is_a_left_unity_wrt H_{4}(Q)
:: according to BINOP_1:def 7 :: thesis: the Element of Q is_a_right_unity_wrt H_{4}(Q)_{4}(Q) . (b, the Element of Q) = b

thus H_{4}(Q) . (b, the Element of Q) = b
by A2; :: thesis: verum

end;thus the Element of Q is_a_left_unity_wrt H

proof

let b be Element of Q; :: according to BINOP_1:def 17 :: thesis: H
let b be Element of Q; :: according to BINOP_1:def 16 :: thesis: H_{4}(Q) . ( the Element of Q,b) = b

thus H_{4}(Q) . ( the Element of Q,b) = b
by A2; :: thesis: verum

end;thus H

thus H

proof

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

thus for a being Element of Q holds a * the Element of Q = the Element of Q by A2; :: thesis: verum

end;proof

take
the Element of Q
; :: according to QUANTAL1:def 3 :: thesis: for a being Element of Q holds a * the Element of Q = the Element of Q
take
the Element of Q
; :: according to QUANTAL1:def 2 :: thesis: for b being Element of Q holds the Element of Q * b = the Element of Q

thus for b being Element of Q holds the Element of Q * b = the Element of Q by A2; :: thesis: verum

end;thus for b being Element of Q holds the Element of Q * b = the Element of Q by A2; :: thesis: verum

thus for a being Element of Q holds a * the Element of Q = the Element of Q by A2; :: thesis: verum

now :: thesis: for X being set ex p9 being Element of Q st

( X is_less_than p9 & ( for r9 being Element of Q st X is_less_than r9 holds

p9 [= r9 ) )

hence
for X being set ex p being Element of Q st ( X is_less_than p9 & ( for r9 being Element of Q st X is_less_than r9 holds

p9 [= r9 ) )

let X be set ; :: thesis: ex p9 being Element of Q st

( X is_less_than p9 & ( for r9 being Element of Q st X is_less_than r9 holds

p9 [= r9 ) )

consider p being Element of (BooleLatt {}) such that

A5: X is_less_than p and

A6: for r being Element of (BooleLatt {}) st X is_less_than r holds

p [= r by LATTICE3:def 18;

reconsider p9 = p as Element of Q by A1;

take p9 = p9; :: thesis: ( X is_less_than p9 & ( for r9 being Element of Q st X is_less_than r9 holds

p9 [= r9 ) )

thus X is_less_than p9 by A1, A5, Th2; :: thesis: for r9 being Element of Q st X is_less_than r9 holds

p9 [= r9

let r9 be Element of Q; :: thesis: ( X is_less_than r9 implies p9 [= r9 )

reconsider r = r9 as Element of (BooleLatt {}) by A1;

assume X is_less_than r9 ; :: thesis: p9 [= r9

then X is_less_than r by A1, Th2;

then p [= r by A6;

hence p9 [= r9 by A1; :: thesis: verum

end;( X is_less_than p9 & ( for r9 being Element of Q st X is_less_than r9 holds

p9 [= r9 ) )

consider p being Element of (BooleLatt {}) such that

A5: X is_less_than p and

A6: for r being Element of (BooleLatt {}) st X is_less_than r holds

p [= r by LATTICE3:def 18;

reconsider p9 = p as Element of Q by A1;

take p9 = p9; :: thesis: ( X is_less_than p9 & ( for r9 being Element of Q st X is_less_than r9 holds

p9 [= r9 ) )

thus X is_less_than p9 by A1, A5, Th2; :: thesis: for r9 being Element of Q st X is_less_than r9 holds

p9 [= r9

let r9 be Element of Q; :: thesis: ( X is_less_than r9 implies p9 [= r9 )

reconsider r = r9 as Element of (BooleLatt {}) by A1;

assume X is_less_than r9 ; :: thesis: p9 [= r9

then X is_less_than r by A1, Th2;

then p [= r by A6;

hence p9 [= r9 by A1; :: thesis: verum

( 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: ( Q is right-distributive & Q is left-distributive & Q is Lattice-like )

thus Q is right-distributive by A2; :: thesis: ( Q is left-distributive & Q is Lattice-like )

thus Q is left-distributive by A2; :: thesis: 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 ; :: thesis: verum