let G be SimpleGraph; :: thesis: (CompleteSGraph (Vertices G)) \ (Edges G) is SimpleGraph
set CSGVG = CompleteSGraph (Vertices G);
set C = (CompleteSGraph (Vertices G)) \ (Edges G);
A1: {} in CompleteSGraph (Vertices G) by Th20;
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
A2: {} = {x,y} by Th11;
thus contradiction by A2; :: thesis: verum
end;
then reconsider C = (CompleteSGraph (Vertices G)) \ (Edges G) as non empty set by A1, 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
A3: X in C and
A4: Y c= X ; :: thesis: Y in C
assume Y nin C ; :: thesis: contradiction
then A5: ( Y nin CompleteSGraph (Vertices G) or Y in Edges G ) by XBOOLE_0:def 5;
A6: ( X in CompleteSGraph (Vertices G) & not X in Edges G ) by A3, XBOOLE_0:def 5;
A7: Y in Edges G by A4, A5, A6, CLASSES1:def 1;
A8: card Y = 2 by A7, Def1;
reconsider X = X as finite set by A3;
A9: card X <= 1 + 1 by A3, Th21;
A10: 2 <= card X by A8, A4, NAT_1:43;
card X = 2 by A9, A10, XXREAL_0:1;
hence contradiction by A6, A5, A4, A8, CARD_2:102; :: thesis: verum
end;
hence (CompleteSGraph (Vertices G)) \ (Edges G) is SimpleGraph ; :: thesis: verum