let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated 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 IC-Ins-separated 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