{} , RelIncl {} are_isomorphic by WELLORD1:48;
hence order_type_of {} is empty by ORDERS_1:119, WELLORD2:def 2; :: thesis: verum