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