let x be Surreal; :: thesis: x is pair
ex A being Ordinal st x in Day A by Def14;
hence x is pair ; :: thesis: verum