RelIncl E = E ;
hence order_type_of E is empty by ORDERS_1:88; :: thesis: verum