let G be SimpleGraph; :: thesis: for x, y being set st y in union G & {[x,(union G)],y} in Mycielskian G holds
{x,y} in G
set MG = Mycielskian G;
set uG = union G;
set A = { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ;
set B = { {(union G),[y,(union G)]} where y is Element of union G : y in union G } ;
let x, y be set ; :: thesis: ( y in union G & {[x,(union G)],y} in Mycielskian G implies {x,y} in G )
assume A1: y in union G ; :: thesis: ( not {[x,(union G)],y} in Mycielskian G or {x,y} in G )
assume {[x,(union G)],y} in Mycielskian G ; :: thesis: {x,y} in G
then {[x,(union G)],y} in ({{}} \/ (singletons (Vertices (Mycielskian G)))) \/ (Edges (Mycielskian G)) by Th27;
then A2: ( {[x,(union G)],y} in {{}} \/ (singletons (Vertices (Mycielskian G))) or {[x,(union G)],y} in Edges (Mycielskian G) ) by XBOOLE_0:def 3;
per cases ( {[x,(union G)],y} in {{}} or {[x,(union G)],y} in singletons (Vertices (Mycielskian G)) or {[x,(union G)],y} in Edges (Mycielskian G) ) by A2, XBOOLE_0:def 3;
suppose {[x,(union G)],y} in {{}} ; :: thesis: {x,y} in G
hence {x,y} in G by TARSKI:def 1; :: thesis: verum
end;
suppose {[x,(union G)],y} in singletons (Vertices (Mycielskian G)) ; :: thesis: {x,y} in G
then consider f being Subset of (Vertices (Mycielskian G)) such that
A3: f = {[x,(union G)],y} and
A4: f is 1 -element ;
consider s being set such that
s in Vertices (Mycielskian G) and
A5: f = {s} by A4, Th9;
A6: card f = 1 by A5, CARD_1:30;
y = [x,(union G)] by A6, A3, CARD_2:57;
hence {x,y} in G by A1, Th1; :: thesis: verum
end;
suppose {[x,(union G)],y} in Edges (Mycielskian G) ; :: thesis: {x,y} in G
then {[x,(union G)],y} in ((Edges G) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[y,(union G)]} where y is Element of union G : y in union G } by Th91;
then A7: ( {[x,(union G)],y} in (Edges G) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } or {[x,(union G)],y} in { {(union G),[y,(union G)]} where y is Element of union G : y in union G } ) by XBOOLE_0:def 3;
per cases ( {[x,(union G)],y} in Edges G or {[x,(union G)],y} in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } or {[x,(union G)],y} in { {(union G),[y,(union G)]} where y is Element of union G : y in union G } ) by A7, XBOOLE_0:def 3;
suppose {[x,(union G)],y} in Edges G ; :: thesis: {x,y} in G
then [x,(union G)] in union G by Th13;
hence {x,y} in G by Th1; :: thesis: verum
end;
suppose {[x,(union G)],y} in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ; :: thesis: {x,y} in G
then consider xx, yy being Element of union G such that
A8: {[x,(union G)],y} = {xx,[yy,(union G)]} and
A9: {xx,yy} in Edges G ;
A10: ( xx in union G & yy in union G ) by A9, Th13;
( ( [x,(union G)] = xx & y = [yy,(union G)] ) or ( [x,(union G)] = [yy,(union G)] & y = xx ) ) by A8, ZFMISC_1:6;
then ( x = yy & y = xx ) by A10, Th1, XTUPLE_0:1;
hence {x,y} in G by A9; :: thesis: verum
end;
suppose {[x,(union G)],y} in { {(union G),[y,(union G)]} where y is Element of union G : y in union G } ; :: thesis: {x,y} in G
then consider yy being Element of union G such that
A11: {[x,(union G)],y} = {(union G),[yy,(union G)]} and
yy in union G ;
( ( [x,(union G)] = union G & y = [yy,(union G)] ) or ( [x,(union G)] = [yy,(union G)] & y = union G ) ) by A11, ZFMISC_1:6;
hence {x,y} in G by Th1, A1; :: thesis: verum
end;
end;
end;
end;