let G be finite _Graph; :: thesis:
let V be VertexScheme of G; :: thesis:
A1: rng V = the_Vertices_of G by Def12;
A2: V is one-to-one by Def12;

A3: now

let a, b, c be Vertex of G; :: thesis:
assume A4: ( b <> c & a,b are_adjacent & a,c are_adjacent & not b,c are_adjacent ) ; :: thesis:
let va, vb, vc be Nat; :: thesis:
assume A5: ( va in dom V & vb in dom V & vc in dom V & V . va = a & V . vb = b & V . vc = c & va < vb & va < vc ) ; :: thesis:
A6: ( a <> b & a <> c ) by A2, A5, FUNCT_1:def 8;
assume A7: V is perfect ; :: thesis:
A8: ( 1 <= va & va <= len V ) by A5, FINSEQ_3:27;
A10: not V .followSet va is empty by A8, Th107;
consider Gf being inducedSubgraph of G,(V .followSet va);
set fs = va,(len V) -cut V;
A11: ((len (va,(len V) -cut V)) + va) - va = ((len V) + 1) - va by A8, GRAPH_2:def 1;
then A12: len (va,(len V) -cut V) = ((len V) - va) + 1 ;
consider jb being Nat such that
A13: va + jb = vb by A5, NAT_1:10;
consider jc being Nat such that
A14: va + jc = vc by A5, NAT_1:10;
va - va <= (len V) - va by A8, XREAL_1:11;
then A15: 0 < len (va,(len V) -cut V) by A12;
then A16: (va,(len V) -cut V) . (0 + 1) = V . (va + 0 ) by A8, GRAPH_2:def 1;

A17: now

assume jb >= len (va,(len V) -cut V) ; :: thesis:
then va + jb >= (((len V) + 1) - va) + va by A11, XREAL_1:9;
then vb > len V by A13, NAT_1:13;
hence contradiction by A5, FINSEQ_3:27; :: thesis:

end;

then A18: (va,(len V) -cut V) . (jb + 1) = V . (va + jb) by A8, GRAPH_2:def 1;

A19: now

assume jc >= len (va,(len V) -cut V) ; :: thesis:
then va + jc >= (((len V) + 1) - va) + va by A11, XREAL_1:9;
then vc > len V by A14, NAT_1:13;
hence contradiction by A5, FINSEQ_3:27; :: thesis:

end;

then A20: (va,(len V) -cut V) . (jc + 1) = V . (va + jc) by A8, GRAPH_2:def 1;
0 + 1 <= len (va,(len V) -cut V) by A15, NAT_1:13;
then 0 + 1 in dom (va,(len V) -cut V) by FINSEQ_3:27;
then A21: a in V .followSet va by A5, A16, FUNCT_1:12;
0 + 1 <= jb + 1 by XREAL_1:9;
then ( 1 <= jb + 1 & jb + 1 <= len (va,(len V) -cut V) ) by A17, NAT_1:13;
then jb + 1 in dom (va,(len V) -cut V) by FINSEQ_3:27;
then A22: b in V .followSet va by A5, A13, A18, FUNCT_1:12;
0 + 1 <= jc + 1 by XREAL_1:9;
then ( 1 <= jc + 1 & jc + 1 <= len (va,(len V) -cut V) ) by A19, NAT_1:13;
then jc + 1 in dom (va,(len V) -cut V) by FINSEQ_3:27;
then A23: c in V .followSet va by A5, A14, A20, FUNCT_1:12;
reconsider ag = a as Vertex of Gf by A21, GLIB_000:def 39;
reconsider bg = b as Vertex of Gf by A22, GLIB_000:def 39;
reconsider cg = c as Vertex of Gf by A23, GLIB_000:def 39;
A24: ag is simplicial by A5, A7, A8, Def13;
A25: ( ag,bg are_adjacent & ag,cg are_adjacent & not bg,cg are_adjacent ) by A4, A10, Th45;
then ( bg in Gf .AdjacentSet {ag} & cg in Gf .AdjacentSet {ag} ) by A6, Th52;
then ex e being set st e Joins bg,cg,Gf by A4, A24, Th68;
hence contradiction by A25, Def3; :: thesis:

end;

now

assume not V is perfect ; :: thesis:
then ex n being non zero Nat st
( n <= len V & ex Gf being inducedSubgraph of G,(V .followSet n) ex v being Vertex of Gf st
( v = V . n & not v is simplicial ) ) by Def13;
then consider n being non zero Nat, Gf being inducedSubgraph of G,(V .followSet n), v being Vertex of Gf such that
A26: ( n <= len V & v = V . n & not v is simplicial ) ;
( 1 <= n & n <= len V ) by A26, Th1;
then A27: n in dom V by FINSEQ_3:27;
consider a, b being Vertex of Gf such that
A28: ( a <> b & v <> a & v <> b ) and
A29: ( v,a are_adjacent & v,b are_adjacent & not a,b are_adjacent ) by A26, Th69;
A30: V .followSet n is non empty Subset of (the_Vertices_of G) by A26, Th107;
then A31: the_Vertices_of Gf = V .followSet n by GLIB_000:def 39;
then reconsider vg = v as Vertex of G by TARSKI:def 3;
A32: a in the_Vertices_of G by A31, TARSKI:def 3;
reconsider ag = a, bg = b as Vertex of G by A31, TARSKI:def 3;
A33: b in the_Vertices_of G by A31, TARSKI:def 3;
A34: ( vg,ag are_adjacent & vg,bg are_adjacent & not ag,bg are_adjacent ) by A29, A30, Th45;
A35: a in rng V by A1, A31, TARSKI:def 3;
consider va being Nat such that
A36: ( va in dom V & V . va = a ) by A1, A32, FINSEQ_2:11;
A37: b in rng V by A1, A31, TARSKI:def 3;
consider vb being Nat such that
A38: ( vb in dom V & V . vb = b ) by A1, A33, FINSEQ_2:11;

A39: now

assume va <= n ; :: thesis:
then A40: va < n by A26, A28, A36, XXREAL_0:1;
a .. V >= n by A2, A27, A31, A35, Th16;
then va < a .. V by A40, XXREAL_0:2;
hence contradiction by A36, FINSEQ_4:34; :: thesis:

end;

now

assume vb <= n ; :: thesis:
then A41: vb < n by A26, A28, A38, XXREAL_0:1;
b .. V >= n by A2, A27, A31, A37, Th16;
then vb < b .. V by A41, XXREAL_0:2;
hence contradiction by A38, FINSEQ_4:34; :: thesis:

end;

hence ex a, b, c being Vertex of G ex va, vb, vc being Nat st
( b <> c & a,b are_adjacent & a,c are_adjacent & va in dom V & vb in dom V & vc in dom V & V . va = a & V . vb = b & V . vc = c & va < vb & va < vc & not b,c are_adjacent ) by A26, A27, A28, A34, A36, A38, A39; :: thesis:

end;

hence ( V is perfect iff for a, b, c being Vertex of G st b <> c & a,b are_adjacent & a,c are_adjacent holds
for va, vb, vc being natural number st va in dom V & vb in dom V & vc in dom V & V . va = a & V . vb = b & V . vc = c & va < vb & va < vc holds
b,c are_adjacent ) by A3; :: thesis: