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 Element of NAT ; :: according to AMISTD_1:def 20 :: thesis: ( not l in proj1 G or for b₁ being Element of NAT holds
( not b₁ <= l,S or b₁ in proj1 G ) )
assume A1: l in dom G ; :: thesis: for b₁ being Element of NAT holds
( not b₁ <= l,S or b₁ in proj1 G )
let m be Element of NAT ; :: thesis: ( not m <= l,S or m in proj1 G )
assume A2: m <= l,S ; :: thesis: m in proj1 G
consider M being non empty finite natural-membered set such that
A3: M = { (locnum w,S) where w is Element of NAT : 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,S in M by A1, A3, A6;
then A8: locnum l,S <= max M by XXREAL_2:def 8;

now

assume m = LastLoc F ; :: thesis: contradiction
then LastLoc F <= il. S,(locnum l,S),S by A2, AMISTD_1:def 13;
then max M <= locnum l,S by A4, AMISTD_1:28;
then il. S,(locnum l,S) = 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 proj1 G by A5, A6, A7, XBOOLE_0:def 5; :: thesis: verum

end;

hence CutLastLoc F is lower ; :: thesis: verum

end;

end;