let G be SimpleGraph; for x, y being object st {[x,(union G)],y} in Edges (Mycielskian G) holds
( x <> y & x in union G & ( y in union G or y = union G ) )
let x, y be object ; ( {[x,(union G)],y} in Edges (Mycielskian G) implies ( x <> y & x in union G & ( y in union G or y = union G ) ) )
assume A1:
{[x,(union G)],y} in Edges (Mycielskian G)
; ( x <> y & x in union G & ( y in union G or y = union G ) )
set uG = union G;
set e = {[x,(union G)],y};
per cases
( {[x,(union G)],y} in Edges G or ex x, y being Element of union G st
( {[x,(union G)],y} = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( {[x,(union G)],y} = {(union G),[y,(union G)]} & y in union G ) )
by A1, Th90;
suppose
ex
x,
y being
Element of
union G st
(
{[x,(union G)],y} = {x,[y,(union G)]} &
{x,y} in Edges G )
;
( x <> y & x in union G & ( y in union G or y = union G ) )then consider xa,
ya being
Element of
union G such that A2:
{[x,(union G)],y} = {xa,[ya,(union G)]}
and A3:
{xa,ya} in Edges G
;
consider xx,
yy being
set such that A4:
xx <> yy
and A5:
(
xx in Vertices G &
yy in Vertices G )
and A6:
{xa,ya} = {xx,yy}
by A3, Th11;
A7:
( (
xa = xx &
ya = yy ) or (
xa = yy &
ya = xx ) )
by A6, ZFMISC_1:6;
end; suppose
ex
y being
Element of
union G st
(
{[x,(union G)],y} = {(union G),[y,(union G)]} &
y in union G )
;
( x <> y & x in union G & ( y in union G or y = union G ) )then consider yy being
Element of
union G such that A8:
{[x,(union G)],y} = {(union G),[yy,(union G)]}
and A9:
yy in union G
;
A10:
( (
union G = [x,(union G)] &
y = [yy,(union G)] ) or (
union G = y &
[x,(union G)] = [yy,(union G)] ) )
by A8, ZFMISC_1:6;
x = yy
by A10, Th2, XTUPLE_0:1;
hence
(
x <> y &
x in union G & (
y in union G or
y = union G ) )
by A10, A9;
verum end; end;