proposition: Lemma ex6_prop5b i (Si := (ex6_systemi i)): inc i L -> [/\ isE Si = restr (isE S) (Vg Jf i), isI Si = Vg Jf i, isr Si = induced_order (isr S) (Vg Jf i)& isf Si = restr (isf S) (induced_order (isr S) (Vg Jf i))].
proof: Proof. by move=> H;rewrite /Si/ex6_systemi; case: (ixm (inc i L)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)