let G be _finite _Graph; :: thesis: for S being VNumberingSeq of G
for m being Nat
for v being set st v in dom (S . m) holds
( (S .Lifespan()) -' ((S . m) . v) < m & (S .Lifespan()) -' m < (S . m) . v )
let S be VNumberingSeq of G; :: thesis: for m being Nat
for v being set st v in dom (S . m) holds
( (S .Lifespan()) -' ((S . m) . v) < m & (S .Lifespan()) -' m < (S . m) . v )
let m be Nat; :: thesis: for v being set st v in dom (S . m) holds
( (S .Lifespan()) -' ((S . m) . v) < m & (S .Lifespan()) -' m < (S . m) . v )
let v be set ; :: thesis: ( v in dom (S . m) implies ( (S .Lifespan()) -' ((S . m) . v) < m & (S .Lifespan()) -' m < (S . m) . v ) )
set VLM = S . m;
set j = (S .Lifespan()) -' ((S . m) . v);
set VLJ = S . ((S .Lifespan()) -' ((S . m) . v));
assume A1: v in dom (S . m) ; :: thesis: ( (S .Lifespan()) -' ((S . m) . v) < m & (S .Lifespan()) -' m < (S . m) . v )
then A2: S .PickedAt ((S .Lifespan()) -' ((S . m) . v)) = v by Th20;
A3: 0 < (S . m) . v by A1, Th15;
A4: (S . m) . v <= S .Lifespan() by Th15;
then (S .Lifespan()) -' ((S . m) . v) = (S .Lifespan()) - ((S . m) . v) by XREAL_1:233;
then A5: (S .Lifespan()) -' ((S . m) . v) < S .Lifespan() by A3, XREAL_1:44;
A6: now :: thesis: (S .Lifespan()) -' ((S . m) . v) < m
per cases ( m <= (S .Lifespan()) -' ((S . m) . v) or m > (S .Lifespan()) -' ((S . m) . v) ) ;
suppose m <= (S .Lifespan()) -' ((S . m) . v) ; :: thesis: (S .Lifespan()) -' ((S . m) . v) < m
then S . m c= S . ((S .Lifespan()) -' ((S . m) . v)) by Th17;
then dom (S . m) c= dom (S . ((S .Lifespan()) -' ((S . m) . v))) by RELAT_1:11;
hence (S .Lifespan()) -' ((S . m) . v) < m by A1, A2, A5, Def9; :: thesis: verum
end;
suppose m > (S .Lifespan()) -' ((S . m) . v) ; :: thesis: (S .Lifespan()) -' ((S . m) . v) < m
hence (S .Lifespan()) -' ((S . m) . v) < m ; :: thesis: verum
end;
end;
end;
now :: thesis: (S .Lifespan()) -' m < (S . m) . v
per cases ( (S .Lifespan()) - m >= 0 or (S .Lifespan()) - m < 0 ) ;
suppose A7: (S .Lifespan()) - m >= 0 ; :: thesis: (S .Lifespan()) -' m < (S . m) . v
(S .Lifespan()) - ((S . m) . v) < m by A4, A6, XREAL_1:233;
then ((S .Lifespan()) - ((S . m) . v)) + ((S . m) . v) < m + ((S . m) . v) by XREAL_1:6;
then (S .Lifespan()) - m < (((S . m) . v) + m) - m by XREAL_1:9;
hence (S .Lifespan()) -' m < (S . m) . v by A7, XREAL_0:def 2; :: thesis: verum
end;
end;
end;
hence ( (S .Lifespan()) -' ((S . m) . v) < m & (S .Lifespan()) -' m < (S . m) . v ) by A6; :: thesis: verum