let G be SimpleGraph; :: thesis: Edges (Mycielskian G) = ((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 }
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 } ;
thus Edges (Mycielskian G) c= ((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 } :: according to XBOOLE_0:def 10 :: thesis: ((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 } c= Edges (Mycielskian G)

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in Edges (Mycielskian G) or e 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 } )
assume A1: e in Edges (Mycielskian G) ; :: thesis: e 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 }

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 A1, Th90;

suppose e in Edges G ; :: thesis: e 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 }

then e in (Edges G) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } by XBOOLE_0:def 3;
hence e 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 XBOOLE_0:def 3; :: thesis: verum

end;

suppose ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) ; :: thesis: e 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 }

then e in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ;
then e in (Edges G) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } by XBOOLE_0:def 3;
hence e 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 XBOOLE_0:def 3; :: thesis: verum

end;

suppose ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) ; :: thesis: e 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 }

then e in { {(union G),[y,(union G)]} where y is Element of union G : y in union G } ;
hence e 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 XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

thus ((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 } c= Edges (Mycielskian G) :: thesis: verum

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e 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 } or e in Edges (Mycielskian G) )
assume e 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 } ; :: thesis: e in Edges (Mycielskian G)
then A2: ( e in (Edges G) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } or e in { {(union G),[y,(union G)]} where y is Element of union G : y in union G } ) by XBOOLE_0:def 3;

per cases ( 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),[y,(union G)]} where y is Element of union G : y in union G } ) by A2, XBOOLE_0:def 3;

suppose e in Edges G ; :: thesis: e in Edges (Mycielskian G)

hence e in Edges (Mycielskian G) by Th90; :: thesis: verum

end;

suppose e in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ; :: thesis: e in Edges (Mycielskian G)

then consider x, y being Element of union G such that
A3: ( e = {x,[y,(union G)]} & {x,y} in Edges G ) ;
thus e in Edges (Mycielskian G) by A3, Th90; :: thesis: verum

end;

suppose e in { {(union G),[y,(union G)]} where y is Element of union G : y in union G } ; :: thesis: e in Edges (Mycielskian G)

then consider y being Element of union G such that
A4: ( e = {(union G),[y,(union G)]} & y in union G ) ;
thus e in Edges (Mycielskian G) by A4, Th90; :: thesis: verum

end;

end;

end;