let G2 be edgeless _Graph; :: thesis: for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w st not v in the_Vertices_of G2 holds
G1 .tChromaticNum() = 3
let v, e be object ; :: thesis: for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w st not v in the_Vertices_of G2 holds
G1 .tChromaticNum() = 3
let w be Vertex of G2; :: thesis: for G1 being addAdjVertex of G2,v,e,w st not v in the_Vertices_of G2 holds
G1 .tChromaticNum() = 3
let G1 be addAdjVertex of G2,v,e,w; :: thesis: ( not v in the_Vertices_of G2 implies G1 .tChromaticNum() = 3 )
assume A1: not v in the_Vertices_of G2 ; :: thesis: G1 .tChromaticNum() = 3
not e in the_Edges_of G2 ;
then not G1 is edgeless by A1, GLIB_006:132, GLIB_008:50;
then A2: 3 c= G1 .tChromaticNum() by Th196;
G1 is 3 -tcolorable by Th174;
then G1 .tChromaticNum() c= 3 by Th189;
hence G1 .tChromaticNum() = 3 by A2, XBOOLE_0:def 10; :: thesis: verum