let G be SimpleGraph; :: thesis: for L being set st L c= Vertices G holds
Vertices (G SubgraphInducedBy L) = L
let L be set ; :: thesis: ( L c= Vertices G implies Vertices (G SubgraphInducedBy L) = L )
assume A1: L c= union G ; :: thesis: Vertices (G SubgraphInducedBy L) = L
thus Vertices (G SubgraphInducedBy L) = (Vertices G) /\ L by Th45
.= L by A1, XBOOLE_1:28 ; :: thesis: verum