let X be set ; :: thesis: for G being finite Graph
for v being Vertex of G st Degree v,X <> 0 holds
not Edges_At v,X is empty
let G be finite Graph; :: thesis: for v being Vertex of G st Degree v,X <> 0 holds
not Edges_At v,X is empty
let v be Vertex of G; :: thesis: ( Degree v,X <> 0 implies not Edges_At v,X is empty )
assume A1: Degree v,X <> 0 ; :: thesis: not Edges_At v,X is empty
assume Edges_At v,X is empty ; :: thesis: contradiction
then ( Edges_In v,X = {} & Edges_Out v,X = {} ) ;
hence contradiction by A1; :: thesis: verum