let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated Mem-Struct of 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 IC-Ins-separated Mem-Struct of 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