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

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