let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of IL,N
for p being FinPartState of S st IC S in dom p holds
Start-At (IC p) c= p
let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated AMI-Struct of IL,N
for p being FinPartState of S st IC S in dom p holds
Start-At (IC p) c= p
let S be non empty IC-Ins-separated AMI-Struct of IL,N; :: thesis: for p being FinPartState of S st IC S in dom p holds
Start-At (IC p) c= p
let p be FinPartState of S; :: thesis: ( IC S in dom p implies Start-At (IC p) c= p )
assume A1: IC S in dom p ; :: thesis: Start-At (IC p) c= p
then A2: IC p = p . (IC S) by Def43;
[(IC S),(p . (IC S))] in p by A1, FUNCT_1:8;
then {[(IC S),(p . (IC S))]} c= p by ZFMISC_1:37;
hence Start-At (IC p) c= p by A2, ZFMISC_1:35; :: thesis: verum