let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being data-only PartState of S
for q being PartState of S holds
( p c= q iff p c= DataPart q )
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p being data-only PartState of S
for q being PartState of S holds
( p c= q iff p c= DataPart q )
let p be data-only PartState of S; :: thesis: for q being PartState of S holds
( p c= q iff p c= DataPart q )
let q be PartState of S; :: thesis: ( p c= q iff p c= DataPart q )
set X = the carrier of S \ ({(IC S)} \/ NAT);
A1: q | ( the carrier of S \ ({(IC S)} \/ NAT)) c= q by RELAT_1:88;

hereby :: thesis: ( p c= DataPart q implies p c= q )

X: ( the carrier of S \ ({(IC S)} \/ NAT)) \/ ({(IC S)} \/ NAT) = the carrier of S \/ ({(IC S)} \/ NAT) by XBOOLE_1:39;
dom p c= the carrier of S by RELAT_1:def 18;
then A2: dom p c= ( the carrier of S \ ({(IC S)} \/ NAT)) \/ ({(IC S)} \/ NAT) by X, XBOOLE_1:10;
assume p c= q ; :: thesis: p c= DataPart q
then A3: p | ( the carrier of S \ ({(IC S)} \/ NAT)) c= DataPart q by RELAT_1:105;
dom p misses {(IC S)} \/ NAT by Def50;
hence p c= DataPart q by A3, A2, RELAT_1:97, XBOOLE_1:73; :: thesis: verum

end;

assume p c= DataPart q ; :: thesis: p c= q
hence p c= q by A1, XBOOLE_1:1; :: thesis: verum