InvLexOrder O is well-ordering by BAGORDER:25;
hence InvLexOrder O is connected by WELLORD1:def 4; :: thesis: verum