let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated Mem-Struct of N
for l being Nat
for p being PartState of S holds
( p is l -started iff Start-At (l,S) c= p )
let S be non empty IC-Ins-separated Mem-Struct of N; :: thesis: for l being Nat
for p being PartState of S holds
( p is l -started iff Start-At (l,S) c= p )
let l be Nat; :: thesis: for p being PartState of S holds
( p is l -started iff Start-At (l,S) c= p )
let p be PartState of S; :: thesis: ( p is l -started iff Start-At (l,S) c= p )
A1: dom (Start-At (l,S)) = {(IC )} by FUNCOP_1:13;
thus ( p is l -started implies Start-At (l,S) c= p ) :: thesis: ( Start-At (l,S) c= p implies p is l -started )

proof

assume A2: p is l -started ; :: thesis: Start-At (l,S) c= p
IC in dom p by A2, Def16;
then A3: dom (Start-At (l,S)) c= dom p by A1, ZFMISC_1:31;
for x being set st x in dom (Start-At (l,S)) holds
(Start-At (l,S)) . x = p . x

proof

let x be set ; :: thesis: ( x in dom (Start-At (l,S)) implies (Start-At (l,S)) . x = p . x )
assume Z: x in dom (Start-At (l,S)) ; :: thesis: (Start-At (l,S)) . x = p . x
hence (Start-At (l,S)) . x = IC (Start-At (l,S)) by A1, TARSKI:def 1
.= l by FUNCOP_1:72
.= IC p by A2, Def16
.= p . x by A1, Z, TARSKI:def 1 ;
:: thesis: verum

end;

hence Start-At (l,S) c= p by A3, GRFUNC_1:2; :: thesis: verum

end;

assume A5: Start-At (l,S) c= p ; :: thesis: p is l -started
then A6: dom (Start-At (l,S)) c= dom p by RELAT_1:11;
A7: IC in dom (Start-At (l,S)) by A1, TARSKI:def 1;
hence IC in dom p by A6; :: according to MEMSTR_0:def 8 :: thesis: IC p = l
thus IC p = IC (Start-At (l,S)) by A5, A7, GRFUNC_1:2
.= l by FUNCOP_1:72 ; :: thesis: verum