let x, y be set ; :: thesis: CompleteSGraph {x,y} = {{},{x},{y},{x,y}}
thus CompleteSGraph {x,y} c= {{},{x},{y},{x,y}} :: according to XBOOLE_0:def 10 :: thesis: {{},{x},{y},{x,y}} c= CompleteSGraph {x,y}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in CompleteSGraph {x,y} or a in {{},{x},{y},{x,y}} )
assume a in CompleteSGraph {x,y} ; :: thesis: a in {{},{x},{y},{x,y}}
then consider V being finite Subset of {x,y} such that
A: a = V and
card V <= 2 ;
( a = {} or a = {x} or a = {y} or a = {x,y} ) by A, ZFMISC_1:36;
hence a in {{},{x},{y},{x,y}} by ENUMSET1:def 2; :: thesis: verum

end;

Aa: {x,y} = Vertices (CompleteSGraph {x,y}) by CSGLem1;
Ab: x in {x,y} by TARSKI:def 2;
Ac: y in {x,y} by TARSKI:def 2;
Ad: card {x,y} <= 2 by CARD_2:50;
Ae: {x,y} c= {x,y} ;
thus {{},{x},{y},{x,y}} c= CompleteSGraph {x,y} :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {{},{x},{y},{x,y}} or a in CompleteSGraph {x,y} )
assume a in {{},{x},{y},{x,y}} ; :: thesis: a in CompleteSGraph {x,y}
then ( a = {} or a = {x} or a = {y} or a = {x,y} ) by ENUMSET1:def 2;
hence a in CompleteSGraph {x,y} by Aa, Ab, Ac, Ad, Ae, SG1, Vertices0; :: thesis: verum

end;