let F be NAT -defined the Instructions of S -valued FinPartState of ; :: thesis: ( F is really-closed & F is initial & not F is empty implies F is para-closed )
assume A1: F is really-closed ; :: thesis: ( not F is initial or F is empty or F is para-closed )
assume ( F is initial & not F is empty ) ; :: thesis: F is para-closed
then 0 in dom F by AFINSQ_1:69;
hence F is para-closed by A1, Th44; :: thesis: verum