let G be SimpleGraph; :: thesis: ( ( for x, y being set st x in Vertices G & y in Vertices G holds
{x,y} in G ) implies G = CompleteSGraph (Vertices G) )
assume A: for x, y being set st x in Vertices G & y in Vertices G holds
{x,y} in G ; :: thesis: G = CompleteSGraph (Vertices G)
set C = { V where V is finite Subset of (Vertices G) : card V <= 2 } ;
{ V where V is finite Subset of (Vertices G) : card V <= 2 } = G

proof

thus { V where V is finite Subset of (Vertices G) : card V <= 2 } c= G :: according to XBOOLE_0:def 10 :: thesis: G c= { V where V is finite Subset of (Vertices G) : card V <= 2 }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { V where V is finite Subset of (Vertices G) : card V <= 2 } or a in G )
assume a in { V where V is finite Subset of (Vertices G) : card V <= 2 } ; :: thesis: a in G
then consider V being finite Subset of (Vertices G) such that
B1: a = V and
C1: card V <= 2 ;

per cases ( card V = 0 or card V = 1 or card V = 2 ) by C1, NAT_1:26;

suppose card V = 0 ; :: thesis: a in G

then V = {} ;
hence a in G by B1, SG1; :: thesis: verum

end;

suppose card V = 1 ; :: thesis: a in G

then consider c being set such that
B2: V = {c} by CARD_2:42;
c in V by B2, TARSKI:def 1;
then {c,c} in G by A;
hence a in G by B2, B1, ENUMSET1:29; :: thesis: verum

end;

suppose card V = 2 ; :: thesis: a in G

then consider c, d being set such that
c <> d and
B2: V = {c,d} by CARD_2:60;
( c in V & d in V ) by B2, TARSKI:def 2;
hence a in G by A, B2, B1; :: thesis: verum

end;

end;

end;

thus G c= { V where V is finite Subset of (Vertices G) : card V <= 2 } :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in G or a in { V where V is finite Subset of (Vertices G) : card V <= 2 } )
assume A1: a in G ; :: thesis: a in { V where V is finite Subset of (Vertices G) : card V <= 2 }
then reconsider aa = a as finite set ;
B1: card aa <= 1 + 1 by A1, Lnatmost1;
a c= union G by A1, ZFMISC_1:74;
hence a in { V where V is finite Subset of (Vertices G) : card V <= 2 } by B1; :: thesis: verum

end;

end;

hence G = CompleteSGraph (Vertices G) ; :: thesis: verum