let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over 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 with_non-empty_values IC-Ins-separated Mem-Struct over 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 )};
A1: q | ( the carrier of S \ {(IC )}) c= q by RELAT_1:59;
hereby :: thesis: ( p c= DataPart q implies p c= q )
A2: ( the carrier of S \ {(IC )}) \/ {(IC )} = the carrier of S \/ {(IC )} by XBOOLE_1:39;
dom p c= the carrier of S by RELAT_1:def 18;
then A3: dom p c= ( the carrier of S \ {(IC )}) \/ {(IC )} by A2, XBOOLE_1:10;
assume p c= q ; :: thesis: p c= DataPart q
then A4: p | ( the carrier of S \ {(IC )}) c= DataPart q by RELAT_1:76;
dom p misses {(IC )} by Def9;
hence p c= DataPart q by A4, A3, RELAT_1:68, XBOOLE_1:73; :: thesis: verum
end;
thus ( p c= DataPart q implies p c= q ) by A1, XBOOLE_1:1; :: thesis: verum