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 ) )
assume A1: LattStr(# the carrier of Q,the L_join of Q,the L_meet of Q #) = BooleLatt {} ; :: thesis: ( Q is cyclic & Q is dualized )
set c = the absurd of Q;
A2: H₁(Q) = {{} } by A1, LATTICE3:def 1, ZFMISC_1:1;
thus Q is cyclic :: thesis: Q is dualized

proof

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 = {} & a -l> the absurd of Q = {} ) by A2, TARSKI:def 1;
hence a -r> the absurd of Q = a -l> the absurd of Q ; :: thesis: verum

end;

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 )
( (a -r> the absurd of Q) -l> the absurd of Q = {} & (a -l> the absurd of Q) -r> the absurd of Q = {} & a = {} ) by A2, 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 ) ; :: thesis: verum