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:11;
(((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:233;
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:233;

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:44;
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:39;
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:11;
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 3;
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:44;
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:44;
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:6; :: 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