let G be SimpleGraph; :: thesis: for x, y being set st {x,y} in G holds
G SubgraphInducedBy {x,y} is Clique of G
let x, y be set ; :: thesis: ( {x,y} in G implies G SubgraphInducedBy {x,y} is Clique of G )
assume A1: {x,y} in G ; :: thesis: G SubgraphInducedBy {x,y} is Clique of G
set S = G SubgraphInducedBy {x,y};

now :: thesis: for a, b being set st a in union (G SubgraphInducedBy {x,y}) & b in union (G SubgraphInducedBy {x,y}) holds
{a,b} in G SubgraphInducedBy {x,y}

let a, b be set ; :: thesis: ( a in union (G SubgraphInducedBy {x,y}) & b in union (G SubgraphInducedBy {x,y}) implies {b₁,b₂} in G SubgraphInducedBy {x,y} )
assume that
A2: a in union (G SubgraphInducedBy {x,y}) and
A3: b in union (G SubgraphInducedBy {x,y}) ; :: thesis: {b₁,b₂} in G SubgraphInducedBy {x,y}
A4: ( a in {x,y} & b in {x,y} ) by A2, A3, Lm7;
then A5: ( ( a = x or a = y ) & ( b = x or b = y ) ) by TARSKI:def 2;

per cases ( a = b or a <> b ) ;

suppose a = b ; :: thesis: {b₁,b₂} in G SubgraphInducedBy {x,y}

then {a,b} = {a} by ENUMSET1:29;
hence {a,b} in G SubgraphInducedBy {x,y} by A2, Th24; :: thesis: verum

end;

suppose a <> b ; :: thesis: {b₁,b₂} in G SubgraphInducedBy {x,y}

hence {a,b} in G SubgraphInducedBy {x,y} by A4, A5, A1, Lm10; :: thesis: verum

end;

end;

end;

then G SubgraphInducedBy {x,y} = CompleteSGraph (Vertices (G SubgraphInducedBy {x,y})) by Th32;
hence G SubgraphInducedBy {x,y} is Clique of G ; :: thesis: verum