let G be finite _Graph; :: thesis: for n being Nat holds ((MCS:CSeq G) . n) `1 is with_property_T
let n be Nat; :: thesis: ((MCS:CSeq G) . n) `1 is with_property_T
set CN = (MCS:CSeq G) . n;
set VLN = ((MCS:CSeq G) . n) `1 ;
set VL = (MCS:CSeq G) ``1 ;

now

let a, b, c be Vertex of G; :: thesis: ( a in dom (((MCS:CSeq G) . n) `1 ) & b in dom (((MCS:CSeq G) . n) `1 ) & c in dom (((MCS:CSeq G) . n) `1 ) & (((MCS:CSeq G) . n) `1 ) . a < (((MCS:CSeq G) . n) `1 ) . b & (((MCS:CSeq G) . n) `1 ) . b < (((MCS:CSeq G) . n) `1 ) . c & a,c are_adjacent & not b,c are_adjacent implies ex d being Vertex of G st
( d in dom (((MCS:CSeq G) . n) `1 ) & (((MCS:CSeq G) . n) `1 ) . b < (((MCS:CSeq G) . n) `1 ) . d & b,d are_adjacent & not a,d are_adjacent ) )
assume that
A1: ( a in dom (((MCS:CSeq G) . n) `1 ) & b in dom (((MCS:CSeq G) . n) `1 ) & c in dom (((MCS:CSeq G) . n) `1 ) ) and
A2: ( (((MCS:CSeq G) . n) `1 ) . a < (((MCS:CSeq G) . n) `1 ) . b & (((MCS:CSeq G) . n) `1 ) . b < (((MCS:CSeq G) . n) `1 ) . c ) and
A3: ( a,c are_adjacent & not b,c are_adjacent ) ; :: thesis: ex d being Vertex of G st
( d in dom (((MCS:CSeq G) . n) `1 ) & (((MCS:CSeq G) . n) `1 ) . b < (((MCS:CSeq G) . n) `1 ) . d & b,d are_adjacent & not a,d are_adjacent )
A4: G .order() = (MCS:CSeq G) .Lifespan() by Th87;
A4a: ((MCS:CSeq G) . n) `1 = ((MCS:CSeq G) ``1 ) . n by d1stMCSLS;
A4b: (MCS:CSeq G) .Lifespan() = ((MCS:CSeq G) ``1 ) .Lifespan() by mVNS0;

now

assume A6: for d being Vertex of G st d in dom (((MCS:CSeq G) . n) `1 ) & (((MCS:CSeq G) . n) `1 ) . b < (((MCS:CSeq G) . n) `1 ) . d & b,d are_adjacent holds
a,d are_adjacent ; :: thesis: contradiction
set bn = (G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b);
set CSB = (MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b));
set VLB = ((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ;
set VL2 = ((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `2 ;
VLBL: ((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 = ((MCS:CSeq G) ``1 ) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) by d1stMCSLS;
(G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b) < n by A4, A4a, A4b, A1, Th29;
then ((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 c= ((MCS:CSeq G) . n) `1 by A4a, VLBL, Th24;
then A7: dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) c= dom (((MCS:CSeq G) . n) `1 ) by RELAT_1:25;
(((MCS:CSeq G) . n) `1 ) . b <= G .order() by A4, A4a, A4b, Th22;
then A8: (G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b) = (G .order() ) - ((((MCS:CSeq G) . n) `1 ) . b) by XREAL_1:235;
then (((MCS:CSeq G) . n) `1 ) . b = (G .order() ) - ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) ;
then A9: (((MCS:CSeq G) . n) `1 ) . b = (G .order() ) -' ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) by XREAL_1:235, NAT_D:35;
A11: 1 <= (((MCS:CSeq G) . n) `1 ) . b by A4a, A1, Th22;
then A12: (G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b) < G .order() by A8, XREAL_1:46;
then A13: dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) <> the_Vertices_of G by Th86;
A14: b = ((MCS:CSeq G) ``1 ) .PickedAt ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) by A4, A1, A4a, A4b, Th27;
then A15: b = MCS:PickUnnumbered ((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) by A8, A11, Th89, XREAL_1:46;

A16: now

assume A17: a in dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) ; :: thesis: contradiction
then (((MCS:CSeq G) . n) `1 ) . b < (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) . a by VLBL, A4, A4b, A9, Th29;
hence contradiction by VLBL, A2, A4a, A1, A17, Th26; :: thesis: verum

end;

A18: (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `2 ) . b = card ((G .AdjacentSet {b}) /\ (dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ))) by A13, A15, Th73, Th91;
not a in dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) by VLBL, A2, A4, A4a, A4b, A1, Th31;
then A19: (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `2 ) . a = card ((G .AdjacentSet {a}) /\ (dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ))) by Th91;
A20: c in dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) by VLBL, A2, A4, A4a, A4b, A1, Th30;
c in G .AdjacentSet {a} by A2, A3, CHORD:52;
then A21: c in (G .AdjacentSet {a}) /\ (dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 )) by A20, XBOOLE_0:def 4;
not c in G .AdjacentSet {b} by A3, CHORD:52;
then A22: not c in (G .AdjacentSet {b}) /\ (dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 )) by XBOOLE_0:def 4;

now

let x be set ; :: thesis: ( x in (G .AdjacentSet {b}) /\ (dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 )) implies x in (G .AdjacentSet {a}) /\ (dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 )) )
assume A23: x in (G .AdjacentSet {b}) /\ (dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 )) ; :: thesis: x in (G .AdjacentSet {a}) /\ (dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ))
A24: x in dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) by A23, XBOOLE_0:def 4;
A26: x in dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) by A23, XBOOLE_0:def 4;
reconsider d = x as Vertex of G by A23;
set CSB1 = (MCS:CSeq G) . (((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) + 1);
set VLB1 = ((MCS:CSeq G) . (((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) + 1)) `1 ;
VLBL1: ((MCS:CSeq G) . (((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) + 1)) `1 = ((MCS:CSeq G) ``1 ) . (((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) + 1) by d1stMCSLS;
then b in dom (((MCS:CSeq G) . (((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) + 1)) `1 ) by A4, A4b, A12, A14, Th18;
then A27: ( (((MCS:CSeq G) . n) `1 ) . b = (((MCS:CSeq G) . (((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) + 1)) `1 ) . b & (((MCS:CSeq G) . n) `1 ) . d = (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) . d ) by VLBL1, VLBL, A4a, A1, A7, A26, Th26;
(G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b) < ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) + 1 by XREAL_1:41;
then ((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 c= ((MCS:CSeq G) . (((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) + 1)) `1 by VLBL, VLBL1, Th24;
then dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) c= dom (((MCS:CSeq G) . (((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) + 1)) `1 ) by RELAT_1:25;
then A28: (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) . d = (((MCS:CSeq G) . (((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) + 1)) `1 ) . d by A24, VLBL1, VLBL, Th26;
(((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) . d in rng (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) by A24, FUNCT_1:def 5;
then (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) . d in (Seg (G .order() )) \ (Seg ((G .order() ) -' ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)))) by A4, A4b, VLBL, Th21;
then (G .order() ) -' ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) < (((MCS:CSeq G) . (((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) + 1)) `1 ) . d by A28, Th5;
then A29: (((MCS:CSeq G) . n) `1 ) . b < (((MCS:CSeq G) . n) `1 ) . d by A4, A4b, VLBL1, A8, A11, A14, A27, A28, Th19, XREAL_1:46;
d in G .AdjacentSet {b} by A23, XBOOLE_0:def 4;
then ( b <> d & b,d are_adjacent ) by CHORD:52;
then a,d are_adjacent by A6, A7, A24, A29;
then d in G .AdjacentSet {a} by A2, A29, CHORD:52;
hence x in (G .AdjacentSet {a}) /\ (dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 )) by A24, XBOOLE_0:def 4; :: thesis: verum

end;

then (G .AdjacentSet {b}) /\ (dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 )) c= (G .AdjacentSet {a}) /\ (dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 )) by TARSKI:def 3;
then (G .AdjacentSet {b}) /\ (dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 )) c< (G .AdjacentSet {a}) /\ (dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 )) by A21, A22, XBOOLE_0:def 8;
hence contradiction by A13, A15, A16, A18, A19, Th72, TREES_1:24; :: thesis: verum

end;

hence ex d being Vertex of G st
( d in dom (((MCS:CSeq G) . n) `1 ) & (((MCS:CSeq G) . n) `1 ) . b < (((MCS:CSeq G) . n) `1 ) . d & b,d are_adjacent & not a,d are_adjacent ) ; :: thesis: verum

end;

hence ((MCS:CSeq G) . n) `1 is with_property_T by Def41; :: thesis: verum