rng {} c= D by XBOOLE_1:2;
hence {} is FinSequence of D by Def4; :: thesis: verum