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 A1: 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 object ; :: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not a in {{},{x}} or a in G SubgraphInducedBy {x} )
reconsider aa = a as set by TARSKI:1;
A2: ( {} in G & {x} in G ) by Th20, A1, Th24;
assume a in {{},{x}} ; :: thesis: a in G SubgraphInducedBy {x}
then A3: ( a = {} or a = {x} ) by TARSKI:def 2;
then aa c= {x} ;
hence a in G SubgraphInducedBy {x} by A2, A3, XBOOLE_0:def 4; :: thesis: verum

end;