let G be _finite _Graph; :: thesis: for i, j being Nat
for a, b being Vertex of G st a in dom (((LexBFS:CSeq G) . i) `1) & b in dom (((LexBFS:CSeq G) . i) `1) & (((LexBFS:CSeq G) . i) `1) . a < (((LexBFS:CSeq G) . i) `1) . b & j = (G .order()) -' ((((LexBFS:CSeq G) . i) `1) . b) holds
(((((LexBFS:CSeq G) . j) `2) . a),1) -bag <= (((((LexBFS:CSeq G) . j) `2) . b),1) -bag , InvLexOrder NAT
let i, j be Nat; :: thesis: for a, b being Vertex of G st a in dom (((LexBFS:CSeq G) . i) `1) & b in dom (((LexBFS:CSeq G) . i) `1) & (((LexBFS:CSeq G) . i) `1) . a < (((LexBFS:CSeq G) . i) `1) . b & j = (G .order()) -' ((((LexBFS:CSeq G) . i) `1) . b) holds
(((((LexBFS:CSeq G) . j) `2) . a),1) -bag <= (((((LexBFS:CSeq G) . j) `2) . b),1) -bag , InvLexOrder NAT
let a, b be Vertex of G; :: thesis: ( a in dom (((LexBFS:CSeq G) . i) `1) & b in dom (((LexBFS:CSeq G) . i) `1) & (((LexBFS:CSeq G) . i) `1) . a < (((LexBFS:CSeq G) . i) `1) . b & j = (G .order()) -' ((((LexBFS:CSeq G) . i) `1) . b) implies (((((LexBFS:CSeq G) . j) `2) . a),1) -bag <= (((((LexBFS:CSeq G) . j) `2) . b),1) -bag , InvLexOrder NAT )
assume that
A1: a in dom (((LexBFS:CSeq G) . i) `1) and
A2: b in dom (((LexBFS:CSeq G) . i) `1) and
A3: (((LexBFS:CSeq G) . i) `1) . a < (((LexBFS:CSeq G) . i) `1) . b and
A4: j = (G .order()) -' ((((LexBFS:CSeq G) . i) `1) . b) ; :: thesis: (((((LexBFS:CSeq G) . j) `2) . a),1) -bag <= (((((LexBFS:CSeq G) . j) `2) . b),1) -bag , InvLexOrder NAT
set VL = (LexBFS:CSeq G) ``1 ;
set CSJ = (LexBFS:CSeq G) . j;
set VLI = ((LexBFS:CSeq G) ``1) . i;
set VLJ = ((LexBFS:CSeq G) ``1) . j;
A5: (((LexBFS:CSeq G) . i) `1) . b = (((LexBFS:CSeq G) ``1) . i) . b by Def15;
A6: a in the_Vertices_of G ;
A7: ((LexBFS:CSeq G) . i) `1 = ((LexBFS:CSeq G) ``1) . i by Def15;
A8: (LexBFS:CSeq G) .Lifespan() = ((LexBFS:CSeq G) ``1) .Lifespan() by Th39;
A9: G .order() = (LexBFS:CSeq G) .Lifespan() by Th37;
then (((LexBFS:CSeq G) ``1) . i) . b <= G .order() by A8, Th15;
then A10: (G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b) = (G .order()) - ((((LexBFS:CSeq G) ``1) . i) . b) by XREAL_1:233;
then A11: (G .order()) -' j = (G .order()) - ((G .order()) - ((((LexBFS:CSeq G) ``1) . i) . b)) by A4, A5, NAT_D:35, XREAL_1:233;

A12: now :: thesis: not a in dom (((LexBFS:CSeq G) . j) `1)

assume a in dom (((LexBFS:CSeq G) . j) `1) ; :: thesis: contradiction
then A13: a in dom (((LexBFS:CSeq G) ``1) . j) by Def15;
then (((LexBFS:CSeq G) ``1) . i) . b < (((LexBFS:CSeq G) ``1) . j) . a by A9, A8, A11, Th22;
hence contradiction by A1, A3, A7, A13, Th19; :: thesis: verum

end;

((LexBFS:CSeq G) ``1) .PickedAt j = b by A2, A4, A7, A9, A8, Th20;
then LexBFS:PickUnnumbered ((LexBFS:CSeq G) . j) = b by A3, A4, A5, A10, Th41, XREAL_1:44;
hence (((((LexBFS:CSeq G) . j) `2) . a),1) -bag <= (((((LexBFS:CSeq G) . j) `2) . b),1) -bag , InvLexOrder NAT by A6, A12, Th29; :: thesis: verum