let G be _finite _Graph; for S being VNumberingSeq of G
for i being Nat
for a, b being set st a in dom (S . i) & (S . i) . a < (S . i) . b holds
not a in dom (S . ((S .Lifespan()) -' ((S . i) . b)))
let S be VNumberingSeq of G; for i being Nat
for a, b being set st a in dom (S . i) & (S . i) . a < (S . i) . b holds
not a in dom (S . ((S .Lifespan()) -' ((S . i) . b)))
let i be Nat; for a, b being set st a in dom (S . i) & (S . i) . a < (S . i) . b holds
not a in dom (S . ((S .Lifespan()) -' ((S . i) . b)))
let a, b be set ; ( a in dom (S . i) & (S . i) . a < (S . i) . b implies not a in dom (S . ((S .Lifespan()) -' ((S . i) . b))) )
assume that
A1:
a in dom (S . i)
and
A2:
(S . i) . a < (S . i) . b
; not a in dom (S . ((S .Lifespan()) -' ((S . i) . b)))
set GN = S .Lifespan() ;
set CSI = S . i;
set VLI = S . i;
set k = (S .Lifespan()) -' ((S . i) . a);
(S . i) . a <= S .Lifespan()
by Th15;
then A3:
(S .Lifespan()) -' ((S . i) . a) = (S .Lifespan()) - ((S . i) . a)
by XREAL_1:233;
set CSK = S . ((S .Lifespan()) -' ((S . i) . a));
set j = (S .Lifespan()) -' ((S . i) . b);
set CSJ = S . ((S .Lifespan()) -' ((S . i) . b));
set VLJ = S . ((S .Lifespan()) -' ((S . i) . b));
set VLK = S . ((S .Lifespan()) -' ((S . i) . a));
(S . i) . b <= S .Lifespan()
by Th15;
then
(S .Lifespan()) -' ((S . i) . b) = (S .Lifespan()) - ((S . i) . b)
by XREAL_1:233;
then
(S .Lifespan()) -' ((S . i) . b) < (S .Lifespan()) -' ((S . i) . a)
by A2, A3, XREAL_1:15;
then
S . ((S .Lifespan()) -' ((S . i) . b)) c= S . ((S .Lifespan()) -' ((S . i) . a))
by Th17;
then A4:
dom (S . ((S .Lifespan()) -' ((S . i) . b))) c= dom (S . ((S .Lifespan()) -' ((S . i) . a)))
by RELAT_1:11;
assume A5:
a in dom (S . ((S .Lifespan()) -' ((S . i) . b)))
; contradiction
1 <= (S . i) . a
by A1, Th15;
then A6:
(S .Lifespan()) -' ((S . i) . a) < S .Lifespan()
by A3, XREAL_1:44;
S .PickedAt ((S .Lifespan()) -' ((S . i) . a)) = a
by A1, Th20;
hence
contradiction
by A6, A5, A4, Def9; verum