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 PartState of S
for k being Nat holds
( Start-At (k,S) c= p iff Start-At (k,S) c= NPP p )
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p being PartState of S
for k being Nat holds
( Start-At (k,S) c= p iff Start-At (k,S) c= NPP p )
let p be PartState of S; :: thesis: for k being Nat holds
( Start-At (k,S) c= p iff Start-At (k,S) c= NPP p )
let k be Nat; :: thesis: ( Start-At (k,S) c= p iff Start-At (k,S) c= NPP p )
thus ( Start-At (k,S) c= p implies Start-At (k,S) c= NPP p ) :: thesis: ( Start-At (k,S) c= NPP p implies Start-At (k,S) c= p )

proof

assume Start-At (k,S) c= p ; :: thesis: Start-At (k,S) c= NPP p
then p is k -started by Th151;
then ( IC p = k & IC in dom p ) by Def16;
then NPP p = (DataPart p) +* (Start-At (k,S)) by Th74;
hence Start-At (k,S) c= NPP p by FUNCT_4:26; :: thesis: verum

end;

thus ( Start-At (k,S) c= NPP p implies Start-At (k,S) c= p ) by XBOOLE_1:1; :: thesis: verum