by_contra hn
case mp.left
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ Set.Nonempty (edgeSet G' \ edgeSet G)
case mp.left
V : Type u_1
G G' : Digraph V
h : G < G'
hn : ¬Set.Nonempty (edgeSet G' \ edgeSet G)
⊢ False