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 A2: Edges_At v,X is empty ; :: thesis: contradiction
then Edges_In v,X = {} ;
hence contradiction by A1, A2; :: thesis: verum