( a c= b or b c= a ) ;
hence a \/ b is Ordinal of W by XBOOLE_1:12; :: thesis: verum