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