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