for x being set st x in On X holds
x is Ordinal by ORDINAL1:def 10;
hence meet (On X) is Ordinal by Th17; :: thesis: verum