defpred S₁[ Element of 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();
not Int-Locations c= L by AMI_3:72;
then consider x being set such that
A2: x in Int-Locations and
A3: not x in L by TARSKI:def 3;
reconsider x = x as Int-Location by A2, SCMFSA_2:11;
consider k being Element of NAT such that
A4: x = intloc k by SCMFSA_2:19;
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