set G = CutLastLoc F;

per cases ( CutLastLoc F is empty or not CutLastLoc F is empty ) ;

suppose CutLastLoc F is empty ; :: thesis: CutLastLoc F is lower

then reconsider H = CutLastLoc F as empty FinPartState of S ;
H is lower ;
hence CutLastLoc F is lower ; :: thesis: verum

end;

suppose not CutLastLoc F is empty ; :: thesis: CutLastLoc F is lower

then reconsider G = CutLastLoc F as non empty FinPartState of S ;
G is lower

proof

let l be Instruction-Location of S; :: according to AMISTD_1:def 20 :: thesis: ( not l in dom G or for b₁ being Instruction-Location of S holds
( not b₁ <= l or b₁ in dom G ) )
assume A1: l in dom G ; :: thesis: for b₁ being Instruction-Location of S holds
( not b₁ <= l or b₁ in dom G )
let m be Instruction-Location of S; :: thesis: ( not m <= l or m in dom G )
assume A2: m <= l ; :: thesis: m in dom G
consider M being non empty finite natural-membered set such that
A3: M = { (locnum w) where w is Instruction-Location of S : w in dom F } and
A4: LastLoc F = il. S,(max M) by AMISTD_1:def 21;
reconsider R = {[(LastLoc F),(F . (LastLoc F))]} as Relation ;
R = (LastLoc F) .--> (F . (LastLoc F)) by FUNCT_4:87;
then A5: dom R = {(LastLoc F)} by FUNCOP_1:19;
then A6: (dom F) \ (dom R) = dom G by Th47;
then A7: m in dom F by A1, A2, AMISTD_1:def 20;
locnum l in M by A1, A3, A6;
then A8: locnum l <= max M by XXREAL_2:def 8;

now

assume m = LastLoc F ; :: thesis: contradiction
then LastLoc F <= il. S,(locnum l) by A2, AMISTD_1:def 13;
then max M <= locnum l by A4, AMISTD_1:28;
then il. S,(locnum l) = il. S,(max M) by A8, XXREAL_0:1;
then LastLoc F in dom G by A1, A4, AMISTD_1:def 13;
then not LastLoc F in {(LastLoc F)} by A5, A6, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

then not m in {(LastLoc F)} by TARSKI:def 1;
hence m in dom G by A5, A6, A7, XBOOLE_0:def 5; :: thesis: verum

end;

hence CutLastLoc F is lower ; :: thesis: verum

end;

end;