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: H1(Q) = {{}} by 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 = {} 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;
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 = {} ) 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