proposition: Lemma show_sub_or : forall b c : E, (nonempty (complement b c) -> nonempty (complement c b) -> False) -> sub b c \/ sub c b.
proof: Proof. exact (fun (b c : E) (H : nonempty (complement b c) -> nonempty (complement c b) -> False) => excluded_middle (fun H0 : sub b c \/ sub c b -> False => H (excluded_middle (fun H1 : nonempty (complement b c) -> False => H0 (or_introl (sub c b) (fun (x : E) (H2 : inc x b) => excluded_middle (fun H3 : inc x c -> False => H1 (nonempty_intro (eq_ind_r (fun P : Prop => P) ( conj H2 H3) (inc_complement b c x)))))))) (excluded_middle (fun H1 : nonempty (complement c b) -> False => H0 (or_intror (sub b c) (fun (x : E) (H2 : inc x c) => excluded_middle (fun H3 : inc x b -> False => H1 (nonempty_intro (eq_ind_r (fun P : Prop => P) ( conj H2 H3) (inc_complement c b x)))))))))). Qed.
imports: universe