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, q being PartState of S st DataPart p c= q holds
DataPart p c= NPP q
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p, q being PartState of S st DataPart p c= q holds
DataPart p c= NPP q
let p, q be PartState of S; :: thesis: ( DataPart p c= q implies DataPart p c= NPP q )
assume DataPart p c= q ; :: thesis: DataPart p c= NPP q
then A: DataPart (DataPart p) c= DataPart q by RELAT_1:105;
DataPart q c= NPP q by Th169;
hence DataPart p c= NPP q by A, XBOOLE_1:1; :: thesis: verum