Relative formal topology, namely, the binary positivity predicate comes first