let G2 be edgeless _Graph; :: thesis: for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not w in the_Vertices_of G2 holds
G1 .tChromaticNum() = 3
let v be Vertex of G2; :: thesis: for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not w in the_Vertices_of G2 holds
G1 .tChromaticNum() = 3
let e, w be object ; :: thesis: for G1 being addAdjVertex of G2,v,e,w st not w in the_Vertices_of G2 holds
G1 .tChromaticNum() = 3
let G1 be addAdjVertex of G2,v,e,w; :: thesis: ( not w in the_Vertices_of G2 implies G1 .tChromaticNum() = 3 )
assume A1: not w 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:131, 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