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