let G be SimpleGraph; for e being set holds
( e in Edges (Mycielskian G) iff ( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) ) )
let e be set ; ( e in Edges (Mycielskian G) iff ( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) ) )
set uG = union G;
set MG = Mycielskian G;
set C = { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ;
set A = { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ;
set B = { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ;
hereby ( ( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) ) implies e in Edges (Mycielskian G) )
assume A1:
e in Edges (Mycielskian G)
;
( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) )then consider x,
y being
set such that A2:
x <> y
and
x in Vertices (Mycielskian G)
and
y in Vertices (Mycielskian G)
and A3:
e = {x,y}
by Th11;
per cases
( e in {{}} or e in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } or e in Edges G or e in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } or e in { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } )
by A1, MYCIELSK:4;
suppose
e in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum }
;
( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) )then consider a being
Element of
((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} such that A4:
e = {a}
;
thus
(
e in Edges G or ex
x,
y being
Element of
union G st
(
e = {x,[y,(union G)]} &
{x,y} in Edges G ) or ex
y being
Element of
union G st
(
e = {(union G),[y,(union G)]} &
y in union G ) )
by A4, A3, A2, ZFMISC_1:5;
verum end; suppose
(
e in Edges G or
e in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } or
e in { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } )
;
( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) )end;
end;
assume A5:
( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) )
; e in Edges (Mycielskian G)
per cases
( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) )
by A5;
suppose
ex
x,
y being
Element of
union G st
(
e = {x,[y,(union G)]} &
{x,y} in Edges G )
;
e in Edges (Mycielskian G)then consider x,
y being
Element of
union G such that A8:
e = {x,[y,(union G)]}
and A9:
{x,y} in Edges G
;
A10:
e in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G }
by A8, A9;
A11:
e in Mycielskian G
by A10, MYCIELSK:4;
y in union G
by A9, Th13;
then
x <> [y,(union G)]
by Th1;
then
card e = 2
by A8, CARD_2:57;
hence
e in Edges (Mycielskian G)
by A11, Def1;
verum end;