reconsider p = <%the Instruction of S%> as FinPartState of S ;
take p ; :: thesis: ( p is initial & not p is empty & p is trivial & p is NAT -defined & p is the Instructions of S -valued )
thus ( p is initial & not p is empty & p is trivial & p is NAT -defined & p is the Instructions of S -valued ) ; :: thesis: verum