reconsider a = {} as FinPartState of S by FUNCT_1:174, RELAT_1:206;
take a ; :: thesis: a is empty
thus a is empty ; :: thesis: verum