fact: Definition Zermelo_ax E (p:fterm) s r:= [/\ worder r, sub (substrate r) E & forall x, inc x (substrate r) -> ( inc (segment r x) s) /\ p (segment r x) = x].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)