take P = pcs-total {{}}; :: thesis: ( P is strict & not P is empty & P is pcs-like )
thus P is strict ; :: thesis: ( not P is empty & P is pcs-like )
thus not the carrier of P is empty ; :: according to STRUCT_0:def 1 :: thesis: P is pcs-like
thus P is pcs-like ; :: thesis: verum