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

b,c are_adjacent )

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

b,c are_adjacent )

A1: V is one-to-one by Def12;

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

( 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 )

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

b,c are_adjacent )

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

A34:
rng V = the_Vertices_of G
by Def12;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 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;

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;

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: contradiction

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: verum

end;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 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: not jc >= len ((va,(len V)) -cut V)

then
jc + 1 <= len ((va,(len V)) -cut V)
by NAT_1:13;assume
jc >= len ((va,(len V)) -cut V)
; :: thesis: contradiction

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: verum

end;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: verum

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: not jb >= len ((va,(len V)) -cut V)

then
jb + 1 <= len ((va,(len V)) -cut V)
by NAT_1:13;assume
jb >= len ((va,(len V)) -cut V)
; :: thesis: contradiction

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: verum

end;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: verum

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: contradiction

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: verum

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 ) )

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 ( 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,(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;

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;

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: verum

end;( 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,(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: not vb <= n

a in the_Vertices_of G
by A39, TARSKI:def 3;assume
vb <= n
; :: thesis: contradiction

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: verum

end;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: verum

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: not va <= n

A58:
not ag,bg are_adjacent
by A45, A38, Th44;assume
va <= n
; :: thesis: contradiction

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: verum

end;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: verum

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: verum

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