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