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