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 object ; :: 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
A1: a = V and
card V <= 2 ;
( a = {} or a = {x} or a = {y} or a = {x,y} ) by A1, ZFMISC_1:36;
hence a in {{},{x},{y},{x,y}} by ENUMSET1:def 2; :: thesis: verum
end;
A2: {x,y} = Vertices (CompleteSGraph {x,y}) by Lm1;
A3: x in {x,y} by TARSKI:def 2;
A4: y in {x,y} by TARSKI:def 2;
A5: card {x,y} <= 2 by CARD_2:50;
thus {{},{x},{y},{x,y}} c= CompleteSGraph {x,y} :: thesis: verum
proof
let a be object ; :: 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 A2, A3, A4, A5, Th20, Th24; :: thesis: verum
end;