Description: Properties of a binary relation with a finite first component with at
least L elements, proven by finite induction on the size of the first
component. This theorem can be applied for graphs (as binary relation
between the set of vertices and an edge function) with a finite number
of vertices, usually with L = 0 (see brfi1ind ) or L = 1 .
(Contributed by Alexander van der Vekens, 7-Jan-2018)(Proof shortened by AV, 23-Oct-2020)(Revised by AV, 28-Mar-2021)