RelIncl X c= [:X,X:] by Th6;
hence RelIncl X is finite ; :: thesis: verum