take the empty FinPartState of S ; :: thesis: ( the empty FinPartState of S is empty & the empty FinPartState of S is NAT -defined )
thus ( the empty FinPartState of S is empty & the empty FinPartState of S is NAT -defined ) ; :: thesis: verum