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;
set V2J = ((LexBFS:CSeq G) . j) `2 ;
A5: (((LexBFS:CSeq G) . i) `1 ) . b = (((LexBFS:CSeq G) ``1 ) . i) . b by Def16;
A6: a in the_Vertices_of G ;
A7: ((LexBFS:CSeq G) . i) `1 = ((LexBFS:CSeq G) ``1 ) . i by Def16;
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:235;
then A11: (G .order() ) -' j = (G .order() ) - ((G .order() ) - ((((LexBFS:CSeq G) ``1 ) . i) . b)) by A4, A5, NAT_D:35, XREAL_1:235;

A12: now

assume a in dom (((LexBFS:CSeq G) . j) `1 ) ; :: thesis: contradiction
then A13: a in dom (((LexBFS:CSeq G) ``1 ) . j) by Def16;
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:46;
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
set CSI = (LexBFS:CSeq G) . i;