let Q be Girard-Quantale; :: thesis: for a being Element of Q holds Bottom (Bottom a) = a
let a be Element of Q; :: thesis: Bottom (Bottom a) = a
the absurd of Q is cyclic by Def19;
then A1: a -l> the absurd of Q = a -r> the absurd of Q ;
the absurd of Q is dualizing by Def20;
hence Bottom (Bottom a) = a by A1; :: thesis: verum