set P = PIStr(# {},({} ({},{})),({} ({},{})) #);
reconsider P = PIStr(# {},({} ({},{})),({} ({},{})) #) as empty strict PIStr ;
take P ; :: thesis: P is PI-preference-like
thus P is PI-preference-like ; :: thesis: verum