reconsider a = {} as PartState of S by FUNCT_1:104, RELAT_1:171;
take a ; :: thesis: a is empty
thus a is empty ; :: thesis: verum