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 ;
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 ;
hence a -r> the absurd of Q = a -l> the absurd of Q by ; :: 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 ;
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 ; :: thesis: verum