let N be 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) 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) 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 [(IC S),(p . (IC S))] in p by FUNCT_1:8;
then A2: {[(IC S),(p . (IC S))]} c= p by ZFMISC_1:37;
IC p = p . (IC S) by A1, Def43;
hence Start-At (IC p) c= p by A2, ZFMISC_1:35; :: thesis: verum