let p be FinPartState of S; :: thesis: ( p is empty implies p is NAT -defined )
assume p is empty ; :: thesis: p is NAT -defined
hence dom p c= NAT by RELAT_1:60, XBOOLE_1:2; :: according to RELAT_1:def 18 :: thesis: verum