let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p, q being PartState of S st Initialize p c= q holds
Start-At (0,S) c= q
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; :: thesis: for p, q being PartState of S st Initialize p c= q holds
Start-At (0,S) c= q
let p, q be PartState of S; :: thesis: ( Initialize p c= q implies Start-At (0,S) c= q )
Start-At (0,S) c= Initialize p by FUNCT_4:25;
hence ( Initialize p c= q implies Start-At (0,S) c= q ) by XBOOLE_1:1; :: thesis: verum