consider p being FinPartState of S;
p in FinPartSt S ;
hence not FinPartSt S is empty ; :: thesis: verum