let G be _finite _Graph; :: thesis:
let V be VertexScheme of G; :: thesis:
A1: V is one-to-one by Def12;

A2: now :: thesis:

let a, b, c be Vertex of G; :: thesis:
assume that
A3: b <> c and
A4: a,b are_adjacent and
A5: a,c are_adjacent and
A6: not b,c are_adjacent ; :: thesis:
let va, vb, vc be Nat; :: thesis:
assume that
A7: va in dom V and
A8: vb in dom V and
A9: vc in dom V and
A10: V . va = a and
A11: V . vb = b and
A12: V . vc = c and
A13: va < vb and
A14: va < vc ; :: thesis:
set Gf = the inducedSubgraph of G,(V .followSet va);
set fs = (va,(len V)) -cut V;
A15: va <= len V by A7, FINSEQ_3:25;
then A16: va - va <= (len V) - va by XREAL_1:9;
A17: 1 <= va by A7, FINSEQ_3:25;
then A18: ((len ((va,(len V)) -cut V)) + va) - va = ((len V) + 1) - va by A15, FINSEQ_6:def 4;
then A19: len ((va,(len V)) -cut V) = ((len V) - va) + 1 ;
then 0 + 1 <= len ((va,(len V)) -cut V) by A16, NAT_1:13;
then A20: 0 + 1 in dom ((va,(len V)) -cut V) by FINSEQ_3:25;
((va,(len V)) -cut V) . (0 + 1) = V . (va + 0) by A17, A15, A19, A16, FINSEQ_6:def 4;
then a in V .followSet va by A10, A20, FUNCT_1:3;
then reconsider ag = a as Vertex of the inducedSubgraph of G,(V .followSet va) by GLIB_000:def 37;
consider jc being Nat such that
A21: va + jc = vc by A14, NAT_1:10;
A22: 0 + 1 <= jc + 1 by XREAL_1:7;

A23: now :: thesis:

assume jc >= len ((va,(len V)) -cut V) ; :: thesis:
then va + jc >= (((len V) + 1) - va) + va by A18, XREAL_1:7;
then vc > len V by A21, NAT_1:13;
hence contradiction by A9, FINSEQ_3:25; :: thesis:

end;

then jc + 1 <= len ((va,(len V)) -cut V) by NAT_1:13;
then A24: jc + 1 in dom ((va,(len V)) -cut V) by A22, FINSEQ_3:25;
((va,(len V)) -cut V) . (jc + 1) = V . (va + jc) by A17, A15, A23, FINSEQ_6:def 4;
then c in V .followSet va by A12, A21, A24, FUNCT_1:3;
then reconsider cg = c as Vertex of the inducedSubgraph of G,(V .followSet va) by GLIB_000:def 37;
A25: not V .followSet va is empty by A17, A15, Th106;
then A26: ag,cg are_adjacent by A5, Th44;
consider jb being Nat such that
A27: va + jb = vb by A13, NAT_1:10;
A28: 0 + 1 <= jb + 1 by XREAL_1:7;

A29: now :: thesis:

assume jb >= len ((va,(len V)) -cut V) ; :: thesis:
then va + jb >= (((len V) + 1) - va) + va by A18, XREAL_1:7;
then vb > len V by A27, NAT_1:13;
hence contradiction by A8, FINSEQ_3:25; :: thesis:

end;

then jb + 1 <= len ((va,(len V)) -cut V) by NAT_1:13;
then A30: jb + 1 in dom ((va,(len V)) -cut V) by A28, FINSEQ_3:25;
((va,(len V)) -cut V) . (jb + 1) = V . (va + jb) by A17, A15, A29, FINSEQ_6:def 4;
then b in V .followSet va by A11, A27, A30, FUNCT_1:3;
then reconsider bg = b as Vertex of the inducedSubgraph of G,(V .followSet va) by GLIB_000:def 37;
A31: not bg,cg are_adjacent by A6, A25, Th44;
assume V is perfect ; :: thesis:
then A32: ag is simplicial by A10, A17, A15;
a <> c by A1, A7, A9, A10, A12, A14, FUNCT_1:def 4;
then A33: cg in the inducedSubgraph of G,(V .followSet va) .AdjacentSet {ag} by A26, Th51;
ag,bg are_adjacent by A4, A25, Th44;
then bg in the inducedSubgraph of G,(V .followSet va) .AdjacentSet {ag} by A26, A31, Th51;
then ex e being object st e Joins bg,cg, the inducedSubgraph of G,(V .followSet va) by A3, A32, A33, Th67;
hence contradiction by A31; :: thesis:

end;

A34: rng V = the_Vertices_of G by Def12;

now :: thesis:

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 ) ) ;
then consider n being non zero Nat, Gf being inducedSubgraph of G,(V .followSet n), v being Vertex of Gf such that
A35: n <= len V and
A36: v = V . n and
A37: not v is simplicial ;
A38: V .followSet n is non empty Subset of (the_Vertices_of G) by A35, Th106;
then A39: the_Vertices_of Gf = V .followSet n by GLIB_000:def 37;
then reconsider vg = v as Vertex of G by TARSKI:def 3;
consider a, b being Vertex of Gf such that
A40: a <> b and
A41: v <> a and
A42: v <> b and
A43: v,a are_adjacent and
A44: v,b are_adjacent and
A45: not a,b are_adjacent by A37, Th68;
reconsider ag = a, bg = b as Vertex of G by A39, TARSKI:def 3;
A46: vg,bg are_adjacent by A44, A38, Th44;
1 <= n by Th1;
then A47: n in dom V by A35, FINSEQ_3:25;
b in the_Vertices_of G by A39, TARSKI:def 3;
then consider vb being Nat such that
A48: vb in dom V and
A49: V . vb = b by A34, FINSEQ_2:10;
A50: b in rng V by A34, A39, TARSKI:def 3;

A51: now :: thesis:

assume vb <= n ; :: thesis:
then A52: vb < n by A36, A42, A49, XXREAL_0:1;
b .. V >= n by A1, A47, A39, A50, Th16;
then vb < b .. V by A52, XXREAL_0:2;
hence contradiction by A48, A49, FINSEQ_4:24; :: thesis:

end;

a in the_Vertices_of G by A39, TARSKI:def 3;
then consider va being Nat such that
A53: va in dom V and
A54: V . va = a by A34, FINSEQ_2:10;
A55: a in rng V by A34, A39, TARSKI:def 3;

A56: now :: thesis:

assume va <= n ; :: thesis:
then A57: va < n by A36, A41, A54, XXREAL_0:1;
a .. V >= n by A1, A47, A39, A55, Th16;
then va < a .. V by A57, XXREAL_0:2;
hence contradiction by A53, A54, FINSEQ_4:24; :: thesis:

end;

A58: not ag,bg are_adjacent by A45, A38, Th44;
vg,ag are_adjacent by A43, A38, Th44;
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 A36, A47, A40, A46, A58, A53, A54, A48, A49, A56, A51; :: 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 Nat 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 A2; :: thesis: