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
A: x <> y and
B: x in Vertices G and
C: 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 D: {x,y} nin Edges ((CompleteSGraph (Vertices G)) \ (Edges G)) ; :: thesis: {x,y} in Edges G
assume E: {x,y} nin Edges G ; :: thesis: contradiction
{x,y} in CompleteSGraph (Vertices G) by B, C, CSG1;
then {x,y} in (CompleteSGraph (Vertices G)) \ (Edges G) by E, XBOOLE_0:def 5;
hence contradiction by D, A, SG4a; :: thesis: verum