let G2 be edgeless _Graph; :: thesis: for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds G1 is 3 -tcolorable
let v, e, w be object ; :: thesis: for G1 being addAdjVertex of G2,v,e,w holds G1 is 3 -tcolorable
let G1 be addAdjVertex of G2,v,e,w; :: thesis: G1 is 3 -tcolorable
( G1 is 2 -vcolorable & G1 is 1 -ecolorable ) by Th38;
then G1 is 2 +` 1 -tcolorable by Th163;
hence G1 is 3 -tcolorable ; :: thesis: verum