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