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 {b1,b2} 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: {b1,b2} 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 ) ;
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