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 CSI = (LexBFS:CSeq G) . i;
set CSJ = (LexBFS:CSeq G) . j;
set VL = (LexBFS:CSeq G) ``1 ;
set VLI = ((LexBFS:CSeq G) ``1 ) . i;
set VLJ = ((LexBFS:CSeq G) ``1 ) . j;
set V2J = ((LexBFS:CSeq G) . j) `2 ;
A4a: (((LexBFS:CSeq G) . i) `1 ) . b = (((LexBFS:CSeq G) ``1 ) . i) . b by d1stBFSLS;
A4b: ((LexBFS:CSeq G) . i) `1 = ((LexBFS:CSeq G) ``1 ) . i by d1stBFSLS;
A7: G .order() = (LexBFS:CSeq G) .Lifespan() by Th51;
A7a: (LexBFS:CSeq G) .Lifespan() = ((LexBFS:CSeq G) ``1 ) .Lifespan() by VNS0;
then (((LexBFS:CSeq G) ``1 ) . i) . b <= G .order() by A7, Th22;
then A8: (G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b) = (G .order() ) - ((((LexBFS:CSeq G) ``1 ) . i) . b) by XREAL_1:235;
then A9: (G .order() ) -' j = (G .order() ) - ((G .order() ) - ((((LexBFS:CSeq G) ``1 ) . i) . b)) by A4, A4a, XREAL_1:235, NAT_D:35;
((LexBFS:CSeq G) ``1 ) .PickedAt j = b by A4, A4b, A2, A7, A7a, Th27;
then A10: LexBFS:PickUnnumbered ((LexBFS:CSeq G) . j) = b by A3, A4, A4a, A8, Th53, XREAL_1:46;
A12: a in the_Vertices_of G ;

now

assume a in dom (((LexBFS:CSeq G) . j) `1 ) ; :: thesis: contradiction
then A13a: a in dom (((LexBFS:CSeq G) ``1 ) . j) by d1stBFSLS;
then (((LexBFS:CSeq G) ``1 ) . i) . b < (((LexBFS:CSeq G) ``1 ) . j) . a by A7, A7a, A9, Th29;
hence contradiction by A3, A4b, A1, A13a, Th26; :: thesis: verum

end;

hence ((((LexBFS:CSeq G) . j) `2 ) . a),1 -bag <= ((((LexBFS:CSeq G) . j) `2 ) . b),1 -bag , InvLexOrder NAT by A10, A12, Th40; :: thesis: verum