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

A1: (MCS:CSeq G) .Lifespan() = ((MCS:CSeq G) ``1 ) .Lifespan() by Th72;
A2: ((MCS:CSeq G) . n) `1 = ((MCS:CSeq G) ``1 ) . n by Def25;
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
A3: a in dom (((MCS:CSeq G) . n) `1 ) and
A4: b in dom (((MCS:CSeq G) . n) `1 ) and
A5: c in dom (((MCS:CSeq G) . n) `1 ) and
A6: (((MCS:CSeq G) . n) `1 ) . a < (((MCS:CSeq G) . n) `1 ) . b and
A7: (((MCS:CSeq G) . n) `1 ) . b < (((MCS:CSeq G) . n) `1 ) . c and
A8: a,c are_adjacent and
A9: 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 )
A10: G .order() = (MCS:CSeq G) .Lifespan() by Th70;

now

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 ;
not c in G .AdjacentSet {b} by A9, CHORD:52;
then A11: not c in (G .AdjacentSet {b}) /\ (dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 )) by XBOOLE_0:def 4;
A12: b = ((MCS:CSeq G) ``1 ) .PickedAt ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) by A4, A10, A2, A1, Th20;
A13: c in G .AdjacentSet {a} by A6, A7, A8, CHORD:52;
A14: ((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 Def25;
then not a in dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) by A3, A6, A10, A2, A1, Th24;
then A15: (((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 Th76;
(G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b) < n by A4, A10, A2, A1, Th22;
then ((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 c= ((MCS:CSeq G) . n) `1 by A2, A14, Th17;
then A16: 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 A10, A2, A1, Th15;
then A17: (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 A18: (((MCS:CSeq G) . n) `1 ) . b = (G .order() ) -' ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) by NAT_D:35, XREAL_1:235;

A19: now

assume A20: 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 A10, A1, A14, A18, Th22;
hence contradiction by A3, A6, A2, A14, A20, Th19; :: thesis: verum

end;

A21: 1 <= (((MCS:CSeq G) . n) `1 ) . b by A4, A2, Th15;
then A22: (G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b) < G .order() by A17, XREAL_1:46;
then A23: dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) <> the_Vertices_of G by Th69;
assume A24: 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

now

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 ;
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 A25: 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 ))
reconsider d = x as Vertex of G by A25;
A26: x in dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) by A25, XBOOLE_0:def 4;
x in dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) by A25, XBOOLE_0:def 4;
then A27: (((MCS:CSeq G) . n) `1 ) . d = (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) . d by A2, A14, A16, Th19;
A28: ((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 Def25;
then b in dom (((MCS:CSeq G) . (((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) + 1)) `1 ) by A10, A1, A22, A12, Th11;
then A29: (((MCS:CSeq G) . n) `1 ) . b = (((MCS:CSeq G) . (((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b)) + 1)) `1 ) . b by A4, A2, A28, Th19;
(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 A14, A28, Th17;
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 A30: (((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 A14, A26, A28, Th19;
(((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 A26, 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 A10, A1, A14, Th14;
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 A30, Th3;
then A31: (((MCS:CSeq G) . n) `1 ) . b < (((MCS:CSeq G) . n) `1 ) . d by A10, A1, A17, A21, A12, A28, A29, A27, A30, Th12, XREAL_1:46;
d in G .AdjacentSet {b} by A25, XBOOLE_0:def 4;
then b,d are_adjacent by CHORD:52;
then a,d are_adjacent by A24, A16, A26, A31;
then d in G .AdjacentSet {a} by A6, A31, CHORD:52;
hence x in (G .AdjacentSet {a}) /\ (dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 )) by A26, XBOOLE_0:def 4; :: thesis: verum

end;

then A32: (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;
c in dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 ) by A4, A5, A7, A10, A2, A1, A14, Th23;
then c in (G .AdjacentSet {a}) /\ (dom (((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) `1 )) by A13, XBOOLE_0:def 4;
then A33: (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 A11, A32, XBOOLE_0:def 8;
A34: b = MCS:PickUnnumbered ((MCS:CSeq G) . ((G .order() ) -' ((((MCS:CSeq G) . n) `1 ) . b))) by A17, A21, A12, Th74, XREAL_1:46;
then (((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 A23, Th59, Th76;
hence contradiction by A23, A34, A19, A15, A33, Th58, 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 Def27; :: thesis: verum