let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated COM-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 COM-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:19;
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:37;
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 x in dom (Start-At (l,S)) ; :: thesis: (Start-At (l,S)) . x = p . x
then A4: x = IC by A1, TARSKI:def 1;
hence (Start-At (l,S)) . x = IC (Start-At (l,S))
.= l by FUNCOP_1:87
.= IC p by A2, Def16
.= p . x by A4 ;
:: thesis: verum

end;

hence Start-At (l,S) c= p by A3, GRFUNC_1:8; :: 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:25;
A7: IC in dom (Start-At (l,S)) by A1, TARSKI:def 1;
hence IC in dom p by A6; :: according to COMPOS_1:def 16 :: thesis: IC p = l
thus IC p = IC (Start-At (l,S)) by A5, A7, GRFUNC_1:8
.= l by FUNCOP_1:87 ; :: thesis: verum