let Q be non empty Girard-QuantaleStr ; :: thesis: ( LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) = BooleLatt {} implies ( Q is cyclic & Q is dualized ) )

set c = the absurd of Q;

assume LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) = BooleLatt {} ; :: thesis: ( Q is cyclic & Q is dualized )

then A1: H_{1}(Q) = {{}}
by LATTICE3:def 1, ZFMISC_1:1;

thus Q is cyclic :: thesis: Q is dualized

( (a -r> the absurd of Q) -l> the absurd of Q = {} & (a -l> the absurd of Q) -r> the absurd of Q = {} ) by A1, TARSKI:def 1;

hence ( (a -r> the absurd of Q) -l> the absurd of Q = a & (a -l> the absurd of Q) -r> the absurd of Q = a ) by A1, TARSKI:def 1; :: thesis: verum

set c = the absurd of Q;

assume LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) = BooleLatt {} ; :: thesis: ( Q is cyclic & Q is dualized )

then A1: H

thus Q is cyclic :: thesis: Q is dualized

proof

let a be Element of Q; :: according to QUANTAL1:def 17,QUANTAL1:def 20 :: thesis: ( (a -r> the absurd of Q) -l> the absurd of Q = a & (a -l> the absurd of Q) -r> the absurd of Q = a )
let a be Element of Q; :: according to QUANTAL1:def 18,QUANTAL1:def 19 :: thesis: a -r> the absurd of Q = a -l> the absurd of Q

a -r> the absurd of Q = {} by A1, TARSKI:def 1;

hence a -r> the absurd of Q = a -l> the absurd of Q by A1, TARSKI:def 1; :: thesis: verum

end;a -r> the absurd of Q = {} by A1, TARSKI:def 1;

hence a -r> the absurd of Q = a -l> the absurd of Q by A1, TARSKI:def 1; :: thesis: verum

( (a -r> the absurd of Q) -l> the absurd of Q = {} & (a -l> the absurd of Q) -r> the absurd of Q = {} ) by A1, TARSKI:def 1;

hence ( (a -r> the absurd of Q) -l> the absurd of Q = a & (a -l> the absurd of Q) -r> the absurd of Q = a ) by A1, TARSKI:def 1; :: thesis: verum