let G be SimpleGraph; :: thesis: for L being set holds Vertices (G SubgraphInducedBy L) = (Vertices G) /\ L
let L be set ; :: thesis: Vertices (G SubgraphInducedBy L) = (Vertices G) /\ L
set S = G SubgraphInducedBy L;
set uS = union (G SubgraphInducedBy L);
set uG = union G;
union (G /\ (bool L)) c= (union G) /\ (union (bool L)) by ZFMISC_1:79;
hence union (G SubgraphInducedBy L) c= (union G) /\ L by ZFMISC_1:81; :: according to XBOOLE_0:def 10 :: thesis: (Vertices G) /\ L c= Vertices (G SubgraphInducedBy L)
thus (union G) /\ L c= union (G SubgraphInducedBy L) :: thesis: verum

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (union G) /\ L or a in union (G SubgraphInducedBy L) )
assume a in (union G) /\ L ; :: thesis: a in union (G SubgraphInducedBy L)
then ( a in union G & a in L ) by XBOOLE_0:def 4;
hence a in union (G SubgraphInducedBy L) by Lm8; :: thesis: verum

end;