seplrcnite fu'ivla

x1 is a Dedekind cut associated with number/point x2 of totally ordered set x3

Let x3 = (X, <) be an ordered set formed by (underlying) set X endowed with order relation '<'. x2 is a member of X; lethe the singleton of x2 (the set containing only and exactly x2) be denoted by Y . Then x1 constitutes an ordered pair of sets (A, B) such that A and B are mutually disjoint subsets of X, A is closed downwardly/lesserwardly under '<', B is closed upwardly/greaterwardly under '<', x2 is not an element of A, and the union of A with B and Y equals exactly X.