proposition: Lemma premaximal_partial_WO_is_full: forall WO:partial_WO, premaximal partial_WO_ord WO -> pwo_S WO = Full_set.
proof: Proof. intros. apply Extensionality_Ensembles. split. unfold Included. intros. constructor. unfold Included. intros. apply NNPP. unfold not; intro. pose (WO' := extend_strictly_partial_WO WO x H1). assert (partial_WO_ord WO' WO). apply H. apply extend_strictly_partial_WO_correct. assert (In (pwo_S WO') x). simpl. constructor 2. auto with sets. apply H1. apply H2. assumption. Qed.
imports: Relation_Definitions Relation_Definitions_Implicit Classical_Wf Description FunctionalExtensionality Classical ZornsLemma ProofIrrelevance EnsemblesSpec