defpred S₁[ Nat] means not intloc $1 in L;
set sn = { k where k is Element of NAT : S₁[k] } ;
A1: { k where k is Element of NAT : S₁[k] } is Subset of NAT from DOMAIN_1:sch 7();
Int-Locations = [:{1},NAT:] by SCM_INST:def 1;
then not Int-Locations c= L ;
then consider x being object such that
A2: x in Int-Locations and
A3: not x in L ;
reconsider x = x as Int-Location by A2, AMI_2:def 16;
consider k being Nat such that
A4: x = intloc k by SCMFSA_2:8;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
k in { k where k is Element of NAT : S₁[k] } by A3, A4;
then reconsider sn = { k where k is Element of NAT : S₁[k] } as non empty Subset of NAT by A1;
take intloc (min sn) ; :: thesis: ex sn being non empty Subset of NAT st
( intloc (min sn) = intloc (min sn) & sn = { k where k is Element of NAT : not intloc k in L } )
take sn ; :: thesis: ( intloc (min sn) = intloc (min sn) & sn = { k where k is Element of NAT : not intloc k in L } )
thus ( intloc (min sn) = intloc (min sn) & sn = { k where k is Element of NAT : not intloc k in L } ) ; :: thesis: verum