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 )
B: dom (Start-At (l,S)) = {(IC S)} 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 Z: p is l -started ; :: thesis: Start-At (l,S) c= p
IC S in dom p by Z, Def41;
then A: dom (Start-At (l,S)) c= dom p by B, 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 C: x = IC S by B, TARSKI:def 1;
hence (Start-At (l,S)) . x = IC (Start-At (l,S))
.= l by FUNCOP_1:87
.= IC p by Z, Def41
.= p . x by C ;
:: thesis: verum

end;

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

end;

assume Z: Start-At (l,S) c= p ; :: thesis: p is l -started
then A: dom (Start-At (l,S)) c= dom p by RELAT_1:25;
C: IC S in dom (Start-At (l,S)) by B, TARSKI:def 1;
hence IC S in dom p by A; :: according to COMPOS_1:def 16 :: thesis: IC p = l
thus IC p = IC (Start-At (l,S)) by Z, C, GRFUNC_1:8
.= l by FUNCOP_1:87 ; :: thesis: verum