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 ( Bottom (Bottom a) = (Bottom a) -r> (Bottom Q) & Bottom a = a -r> (Bottom Q) & Bottom Q = the absurd of Q & a -l> the absurd of Q = a -r> the absurd of Q & the absurd of Q is dualizing ) by Def18, Def20;
hence Bottom (Bottom a) = a by Def17; :: thesis: verum