let G be finite _Graph; :: thesis: for V being VertexScheme of G holds
( 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

let V be VertexScheme of G; :: thesis: ( 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

A1: V is one-to-one by Def12;
A2: now :: thesis: for a, b, c being Vertex of G st b <> c & a,b are_adjacent & a,c are_adjacent & not b,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
not V is perfect
let a, b, c be Vertex of G; :: thesis: ( b <> c & a,b are_adjacent & a,c are_adjacent & not b,c are_adjacent implies 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
not V is perfect )

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: 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
not V is perfect

let va, vb, vc be Nat; :: thesis: ( 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 implies not V is perfect )
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: not V is perfect
set Gf = the inducedSubgraph of G,(V .followSet va);
set fs = (va,(len V)) -cut V;
A15: va <= len V by ;
then A16: va - va <= (len V) - va by XREAL_1:9;
A17: 1 <= va by ;
then A18: ((len ((va,(len V)) -cut V)) + va) - va = ((len V) + 1) - va by ;
then A19: len ((va,(len V)) -cut V) = ((len V) - va) + 1 ;
then 0 + 1 <= len ((va,(len V)) -cut V) by ;
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 ;
then a in V .followSet va by ;
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 ;
A22: 0 + 1 <= jc + 1 by XREAL_1:7;
A23: now :: thesis: not jc >= len ((va,(len V)) -cut V)
assume jc >= len ((va,(len V)) -cut V) ; :: thesis: contradiction
then va + jc >= (((len V) + 1) - va) + va by ;
then vc > len V by ;
hence contradiction by A9, FINSEQ_3:25; :: thesis: verum
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 ;
((va,(len V)) -cut V) . (jc + 1) = V . (va + jc) by ;
then c in V .followSet va by ;
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 ;
then A26: ag,cg are_adjacent by ;
consider jb being Nat such that
A27: va + jb = vb by ;
A28: 0 + 1 <= jb + 1 by XREAL_1:7;
A29: now :: thesis: not jb >= len ((va,(len V)) -cut V)
assume jb >= len ((va,(len V)) -cut V) ; :: thesis: contradiction
then va + jb >= (((len V) + 1) - va) + va by ;
then vb > len V by ;
hence contradiction by A8, FINSEQ_3:25; :: thesis: verum
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 ;
((va,(len V)) -cut V) . (jb + 1) = V . (va + jb) by ;
then b in V .followSet va by ;
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 ;
assume V is perfect ; :: thesis: contradiction
then A32: ag is simplicial by ;
a <> c by ;
then A33: cg in the inducedSubgraph of G,(V .followSet va) .AdjacentSet {ag} by ;
ag,bg are_adjacent by ;
then bg in the inducedSubgraph of G,(V .followSet va) .AdjacentSet {ag} by ;
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: verum
end;
A34: rng V = the_Vertices_of G by Def12;
now :: thesis: ( not V is perfect implies 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 ) )
assume not V is perfect ; :: thesis: 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 )

then ex n being non zero Nat st
( n <= len V & ex Gf being inducedSubgraph of G,() 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 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 () by ;
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 ;
reconsider ag = a, bg = b as Vertex of G by ;
A46: vg,bg are_adjacent by ;
1 <= n by Th1;
then A47: n in dom V by ;
b in the_Vertices_of G by ;
then consider vb being Nat such that
A48: vb in dom V and
A49: V . vb = b by ;
A50: b in rng V by ;
A51: now :: thesis: not vb <= n
assume vb <= n ; :: thesis: contradiction
then A52: vb < n by ;
b .. V >= n by A1, A47, A39, A50, Th16;
then vb < b .. V by ;
hence contradiction by A48, A49, FINSEQ_4:24; :: thesis: verum
end;
a in the_Vertices_of G by ;
then consider va being Nat such that
A53: va in dom V and
A54: V . va = a by ;
A55: a in rng V by ;
A56: now :: thesis: not va <= n
assume va <= n ; :: thesis: contradiction
then A57: va < n by ;
a .. V >= n by A1, A47, A39, A55, Th16;
then va < a .. V by ;
hence contradiction by A53, A54, FINSEQ_4:24; :: thesis: verum
end;
A58: not ag,bg are_adjacent by ;
vg,ag are_adjacent by ;
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: verum
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: verum