fact: Record partial_WO : Type := { pwo_S: Ensemble T; pwo_R: relation T; pwo_R_lives_on_S: forall (x y:T), pwo_R x y -> In pwo_S x /\ In pwo_S y; pwo_wo: well_order (restriction_relation pwo_R pwo_S) }.
imports: Relation_Definitions Relation_Definitions_Implicit Classical_Wf Description FunctionalExtensionality Classical ZornsLemma ProofIrrelevance EnsemblesSpec