let G be SimpleGraph; :: thesis: for x, y being set st x <> y & x in Vertices G & y in Vertices G holds
( {x,y} in Edges G iff {x,y} nin Edges ((CompleteSGraph (Vertices G)) \ (Edges G)) )
let x, y be set ; :: thesis: ( x <> y & x in Vertices G & y in Vertices G implies ( {x,y} in Edges G iff {x,y} nin Edges ((CompleteSGraph (Vertices G)) \ (Edges G)) ) )
assume that
A1: x <> y and
A2: x in Vertices G and
A3: y in Vertices G ; :: thesis: ( {x,y} in Edges G iff {x,y} nin Edges ((CompleteSGraph (Vertices G)) \ (Edges G)) )
set CG = (CompleteSGraph (Vertices G)) \ (Edges G);
thus ( {x,y} in Edges G implies {x,y} nin Edges ((CompleteSGraph (Vertices G)) \ (Edges G)) ) by XBOOLE_0:def 5; :: thesis: ( {x,y} nin Edges ((CompleteSGraph (Vertices G)) \ (Edges G)) implies {x,y} in Edges G )
assume A4: {x,y} nin Edges ((CompleteSGraph (Vertices G)) \ (Edges G)) ; :: thesis: {x,y} in Edges G
assume A5: {x,y} nin Edges G ; :: thesis: contradiction
{x,y} in CompleteSGraph (Vertices G) by A2, A3, Th34;
then {x,y} in (CompleteSGraph (Vertices G)) \ (Edges G) by A5, XBOOLE_0:def 5;
hence contradiction by A4, A1, Th12; :: thesis: verum