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 being PartState of S
for x being set holds
( not x in dom (Initialize p) or x in dom p or x = IC )
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; :: thesis: for p being PartState of S
for x being set holds
( not x in dom (Initialize p) or x in dom p or x = IC )
let p be PartState of S; :: thesis: for x being set holds
( not x in dom (Initialize p) or x in dom p or x = IC )
let x be set ; :: thesis: ( not x in dom (Initialize p) or x in dom p or x = IC )
assume A1: x in dom (Initialize p) ; :: thesis: ( x in dom p or x = IC )
dom (Initialize p) = (dom p) \/ {(IC )} by Th42;
then ( x in dom p or x in {(IC )} ) by A1, XBOOLE_0:def 3;
hence ( x in dom p or x = IC ) by TARSKI:def 1; :: thesis: verum