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