take P = TolStr(# {{}},({} ({{}},{{}})) #); :: thesis: ( P is strict & not P is empty & P is pcs-tol-irreflexive & P is pcs-tol-symmetric )
thus P is strict ; :: thesis: ( not P is empty & P is pcs-tol-irreflexive & P is pcs-tol-symmetric )
thus not the carrier of P is empty ; :: according to STRUCT_0:def 1 :: thesis: ( P is pcs-tol-irreflexive & P is pcs-tol-symmetric )
thus ( P is pcs-tol-irreflexive & P is pcs-tol-symmetric ) ; :: thesis: verum