take F_Real ; :: thesis: F_Real is preordered
thus F_Real is preordered by EX; :: thesis: verum