let G be SimpleGraph; :: thesis: for x being set st x in Vertices G holds
G SubgraphInducedBy {x} = {{},{x}}
let x be set ; :: thesis: ( x in Vertices G implies G SubgraphInducedBy {x} = {{},{x}} )
assume A: x in Vertices G ; :: thesis: G SubgraphInducedBy {x} = {{},{x}}
set Gx = G SubgraphInducedBy {x};
thus G SubgraphInducedBy {x} c= {{},{x}} :: according to XBOOLE_0:def 10 :: thesis: {{},{x}} c= G SubgraphInducedBy {x}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in G SubgraphInducedBy {x} or a in {{},{x}} )
assume a in G SubgraphInducedBy {x} ; :: thesis: a in {{},{x}}
then a in bool {x} by XBOOLE_0:def 4;
then ( a = {} or a = {x} ) by ZFMISC_1:33;
hence a in {{},{x}} by TARSKI:def 2; :: thesis: verum

end;

thus {{},{x}} c= G SubgraphInducedBy {x} :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {{},{x}} or a in G SubgraphInducedBy {x} )
A1: ( {} in G & {x} in G ) by SG1, A, Vertices0;
assume a in {{},{x}} ; :: thesis: a in G SubgraphInducedBy {x}
then B1: ( a = {} or a = {x} ) by TARSKI:def 2;
then a c= {x} by ZFMISC_1:33;
hence a in G SubgraphInducedBy {x} by A1, B1, XBOOLE_0:def 4; :: thesis: verum

end;