let G be SimpleGraph; :: thesis: for x, y being object st x <> y holds
not {[x,(union G)],[y,(union G)]} in Mycielskian G
let x, y be object ; :: thesis: ( x <> y implies not {[x,(union G)],[y,(union G)]} in Mycielskian G )
assume that
A1: x <> y and
A2: {[x,(union G)],[y,(union G)]} in Mycielskian G ; :: thesis: contradiction
[x,(union G)] <> [y,(union G)] by A1, XTUPLE_0:1;
then card {[x,(union G)],[y,(union G)]} = 2 by CARD_2:57;
then {[x,(union G)],[y,(union G)]} in Edges (Mycielskian G) by A2, Def1;
hence contradiction by Th97; :: thesis: verum