for x being object st x in On X holds
x is Ordinal by ORDINAL1:def 9;
hence meet (On X) is Ordinal by Th13; :: thesis: verum