let IL, N be set ; :: thesis: for S being non empty AMI-Struct of IL,N
for p being data-only FinPartState of S holds ProgramPart p = {}
let S be non empty AMI-Struct of IL,N; :: thesis: for p being data-only FinPartState of S holds ProgramPart p = {}
let p be data-only FinPartState of S; :: thesis: ProgramPart p = {}
dom p misses {(IC S)} \/ IL by Def50;
then dom p misses IL by XBOOLE_1:70;
hence ProgramPart p = {} by RELAT_1:187; :: thesis: verum