take First*NotIn (UsedInt*Loc p) ; :: thesis: ex sil being finite Subset of FinSeq-Locations st
( sil = UsedInt*Loc p & First*NotIn (UsedInt*Loc p) = First*NotIn sil )
take UsedInt*Loc p ; :: thesis: ( UsedInt*Loc p = UsedInt*Loc p & First*NotIn (UsedInt*Loc p) = First*NotIn (UsedInt*Loc p) )
thus ( UsedInt*Loc p = UsedInt*Loc p & First*NotIn (UsedInt*Loc p) = First*NotIn (UsedInt*Loc p) ) ; :: thesis: verum