field (RelIncl X) = X by ORDERS_1:12;
hence InclPoset X is connected by RELAT_2:def 14, ORDERS_5:def 1; :: thesis: verum