let G be _Graph; :: thesis: for v being Vertex of G st 4 c= G .order() & v is endvertex holds
ex x, y, z being Vertex of G st
( v <> x & v <> y & v <> z & x <> y & x <> z & y <> z & v,x are_adjacent & not v,y are_adjacent & not v,z are_adjacent )
let v be Vertex of G; :: thesis: ( 4 c= G .order() & v is endvertex implies ex x, y, z being Vertex of G st
( v <> x & v <> y & v <> z & x <> y & x <> z & y <> z & v,x are_adjacent & not v,y are_adjacent & not v,z are_adjacent ) )
assume A1: ( 4 c= G .order() & v is endvertex ) ; :: thesis: ex x, y, z being Vertex of G st
( v <> x & v <> y & v <> z & x <> y & x <> z & y <> z & v,x are_adjacent & not v,y are_adjacent & not v,z are_adjacent )
Segm 3 c= Segm 4 by NAT_1:39;
then consider x, y being Vertex of G such that
A2: ( x <> v & y <> v & x <> y & x,v are_adjacent & not v,y are_adjacent ) by A1, Th101, XBOOLE_1:1;
consider z being object such that
A3: ( z in the_Vertices_of G & v <> z & x <> z & y <> z ) by A1, Th21;
reconsider z = z as Vertex of G by A3;
take x ; :: thesis: ex y, z being Vertex of G st
( v <> x & v <> y & v <> z & x <> y & x <> z & y <> z & v,x are_adjacent & not v,y are_adjacent & not v,z are_adjacent )
take y ; :: thesis: ex z being Vertex of G st
( v <> x & v <> y & v <> z & x <> y & x <> z & y <> z & v,x are_adjacent & not v,y are_adjacent & not v,z are_adjacent )
take z ; :: thesis: ( v <> x & v <> y & v <> z & x <> y & x <> z & y <> z & v,x are_adjacent & not v,y are_adjacent & not v,z are_adjacent )
thus ( v <> x & v <> y & v <> z & x <> y & x <> z & y <> z ) by A2, A3; :: thesis: ( v,x are_adjacent & not v,y are_adjacent & not v,z are_adjacent )
thus v,x are_adjacent by A2; :: thesis: ( not v,y are_adjacent & not v,z are_adjacent )
thus not v,y are_adjacent by A2; :: thesis: not v,z are_adjacent
thus not v,z are_adjacent by A1, A2, A3, Th100; :: thesis: verum