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 being data-only FinPartState of S
for q being FinPartState of S holds
( p c= q iff p c= DataPart 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 being data-only FinPartState of S
for q being FinPartState of S holds
( p c= q iff p c= DataPart q )
let S be non empty IC-Ins-separated AMI-Struct of IL,N; :: thesis: for p being data-only FinPartState of S
for q being FinPartState of S holds
( p c= q iff p c= DataPart q )
let p be data-only FinPartState of S; :: thesis: for q being FinPartState of S holds
( p c= q iff p c= DataPart q )
let q be FinPartState of S; :: thesis: ( p c= q iff p c= DataPart q )
set X = the carrier of S \ ({(IC S)} \/ IL);

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

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

end;

assume A5: p c= DataPart q ; :: thesis: p c= q
q | (the carrier of S \ ({(IC S)} \/ IL)) c= q by RELAT_1:88;
hence p c= q by A5, XBOOLE_1:1; :: thesis: verum