let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N
for p being FinPartState of S st IC S in dom p holds
not p is IL -defined
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N
for p being FinPartState of S st IC S in dom p holds
not p is IL -defined
let S be non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N; :: thesis: for p being FinPartState of S st IC S in dom p holds
not p is IL -defined
let p be FinPartState of S; :: thesis: ( IC S in dom p implies not p is IL -defined )
assume A1: IC S in dom p ; :: thesis: not p is IL -defined
assume p is IL -defined ; :: thesis: contradiction
then dom p = dom (ProgramPart p) by Th105;
hence contradiction by A1, Th101; :: thesis: verum