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