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 A1: 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 object ; :: 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
A2: a = V and
A3: card V <= 2 ;
not not card V = 0 & ... & not card V = 2 by A3;

per cases then ( card V = 0 or card V = 1 or card V = 2 ) ;

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

then V = {} ;
hence a in G by A2, Th20; :: thesis: verum

end;

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

then consider c being object such that
A4: V = {c} by CARD_2:42;
c in V by A4, TARSKI:def 1;
then {c,c} in G by A1;
hence a in G by A4, A2, ENUMSET1:29; :: thesis: verum

end;

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

then consider c, d being object such that
c <> d and
A5: V = {c,d} by CARD_2:60;
( c in V & d in V ) by A5, TARSKI:def 2;
hence a in G by A1, A5, A2; :: 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 object ; :: 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 A6: 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 ;
A7: card aa <= 1 + 1 by A6, Th21;
aa c= union G by A6, ZFMISC_1:74;
hence a in { V where V is finite Subset of (Vertices G) : card V <= 2 } by A7; :: thesis: verum

end;

end;

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