let G be _finite _Graph; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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))) ; :: thesis: 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; :: thesis: verum