let G be SimpleGraph; :: thesis: for L being set holds G SubgraphInducedBy L = G SubgraphInducedBy (L /\ (Vertices G))
let L be set ; :: thesis: G SubgraphInducedBy L = G SubgraphInducedBy (L /\ (Vertices G))
thus G SubgraphInducedBy L c= G SubgraphInducedBy (L /\ (Vertices G)) :: according to XBOOLE_0:def 10 :: thesis: G SubgraphInducedBy (L /\ (Vertices G)) c= G SubgraphInducedBy L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in G SubgraphInducedBy L or x in G SubgraphInducedBy (L /\ (Vertices G)) )
reconsider xx = x as set by TARSKI:1;
assume A1: x in G SubgraphInducedBy L ; :: thesis: x in G SubgraphInducedBy (L /\ (Vertices G))
then A2: x in bool L by XBOOLE_0:def 4;
A3: xx c= Vertices G by A1, ZFMISC_1:74;
A4: xx c= L /\ (Vertices G) by A2, A3, XBOOLE_1:19;
thus x in G SubgraphInducedBy (L /\ (Vertices G)) by A1, A4, XBOOLE_0:def 4; :: thesis: verum

end;

thus G SubgraphInducedBy (L /\ (Vertices G)) c= G SubgraphInducedBy L :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in G SubgraphInducedBy (L /\ (Vertices G)) or x in G SubgraphInducedBy L )
reconsider xx = x as set by TARSKI:1;
assume A5: x in G SubgraphInducedBy (L /\ (Vertices G)) ; :: thesis: x in G SubgraphInducedBy L
then x in bool (L /\ (Vertices G)) by XBOOLE_0:def 4;
then A6: xx c= L by XBOOLE_1:18;
thus x in G SubgraphInducedBy L by A5, A6, XBOOLE_0:def 4; :: thesis: verum

end;