let G be SimpleGraph; :: thesis: (CompleteSGraph (Vertices G)) \ (Edges G) is SimpleGraph
set CSGVG = CompleteSGraph (Vertices G);
set C = (CompleteSGraph (Vertices G)) \ (Edges G);
Z1: {} in CompleteSGraph (Vertices G) by SG1;

now :: thesis: not {} in Edges G

assume {} in Edges G ; :: thesis: contradiction
then consider x, y being set such that
( x <> y & x in Vertices G & y in Vertices G ) and
A1: {} = {x,y} by SG4;
thus contradiction by A1; :: thesis: verum

end;

then reconsider C = (CompleteSGraph (Vertices G)) \ (Edges G) as non empty set by Z1, XBOOLE_0:def 5;
C is subset-closed

proof

let X, Y be set ; :: according to CLASSES1:def 1 :: thesis: ( not X in C or not Y c= X or Y in C )
assume that
A1: X in C and
B1: Y c= X ; :: thesis: Y in C
assume Y nin C ; :: thesis: contradiction
then C1: ( Y nin CompleteSGraph (Vertices G) or Y in Edges G ) by XBOOLE_0:def 5;
D1: ( X in CompleteSGraph (Vertices G) & not X in Edges G ) by A1, XBOOLE_0:def 5;
E1: Y in Edges G by B1, C1, D1, CLASSES1:def 1;
F1: card Y = 2 by E1, LEdges;
reconsider X = X as finite set by A1;
G1: card X <= 1 + 1 by A1, Lnatmost1;
H1: 2 <= card X by F1, B1, NAT_1:43;
card X = 2 by G1, H1, XXREAL_0:1;
hence contradiction by D1, C1, B1, F1, CARD_FIN:1; :: thesis: verum

end;

hence (CompleteSGraph (Vertices G)) \ (Edges G) is SimpleGraph ; :: thesis: verum