the carrier of (pcs-reverse P) = the carrier of P by Def40;
hence not the carrier of (pcs-reverse P) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum