let x be set ; :: thesis: CompleteSGraph {x} = {{},{x}}
thus CompleteSGraph {x} c= {{},{x}} :: according to XBOOLE_0:def 10 :: thesis: {{},{x}} c= CompleteSGraph {x}
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in CompleteSGraph {x} or a in {{},{x}} )
assume a in CompleteSGraph {x} ; :: thesis: a in {{},{x}}
then consider V being finite Subset of {x} such that
A1: a = V and
card V <= 2 ;
( a = {} or a = {x} ) by A1, ZFMISC_1:33;
hence a in {{},{x}} by TARSKI:def 2; :: thesis: verum
end;
A2: {x} = Vertices (CompleteSGraph {x}) by Lm1;
A3: x in {x} by TARSKI:def 1;
thus {{},{x}} c= CompleteSGraph {x} :: thesis: verum
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {{},{x}} or a in CompleteSGraph {x} )
assume a in {{},{x}} ; :: thesis: a in CompleteSGraph {x}
then ( a = {} or a = {x} ) by TARSKI:def 2;
hence a in CompleteSGraph {x} by A2, A3, Th20, Th24; :: thesis: verum
end;