let F be NAT -defined the Instructions of S -valued finite Function; :: thesis: ( F is really-closed & F is lower & not F is empty implies F is para-closed )
assume A1: F is really-closed ; :: thesis: ( not F is lower or F is empty or F is para-closed )
assume ( F is lower & not F is empty ) ; :: thesis: F is para-closed
then il. (S,0) in dom F by Th49;
hence F is para-closed by A1, Th44; :: thesis: verum