take
<*> the carrier of A
; :: thesis: ( <*> the carrier of A is empty & <*> the carrier of A is ascending & <*> the carrier of A is weakly-ascending & <*> the carrier of A is descending & <*> the carrier of A is weakly-descending )

thus ( <*> the carrier of A is empty & <*> the carrier of A is ascending & <*> the carrier of A is weakly-ascending & <*> the carrier of A is descending & <*> the carrier of A is weakly-descending ) ; :: thesis: verum

thus ( <*> the carrier of A is empty & <*> the carrier of A is ascending & <*> the carrier of A is weakly-ascending & <*> the carrier of A is descending & <*> the carrier of A is weakly-descending ) ; :: thesis: verum