let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of IL,N
for p, q being FinPartState of S holds dom (DataPart p) misses dom (ProgramPart q)
let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated AMI-Struct of IL,N
for p, q being FinPartState of S holds dom (DataPart p) misses dom (ProgramPart q)
let S be non empty IC-Ins-separated AMI-Struct of IL,N; :: thesis: for p, q being FinPartState of S holds dom (DataPart p) misses dom (ProgramPart q)
let p, q be FinPartState of S; :: thesis: dom (DataPart p) misses dom (ProgramPart q)
A1: the carrier of S \ ({(IC S)} \/ IL) c= the carrier of S \ IL by XBOOLE_1:7, XBOOLE_1:34;
dom (DataPart p) c= the carrier of S \ ({(IC S)} \/ IL) by RELAT_1:87;
then A2: dom (DataPart p) c= the carrier of S \ IL by A1, XBOOLE_1:1;
dom (ProgramPart q) c= IL by RELAT_1:87;
hence dom (DataPart p) misses dom (ProgramPart q) by A2, XBOOLE_1:64, XBOOLE_1:79; :: thesis: verum