let A be Ordinal; :: thesis: inf A = {}
A1: inf A = meet A by ORDINAL2:8;
then ( A <> {} implies inf A = {} ) by Th8, SETFAM_1:4;
hence inf A = {} by A1, SETFAM_1:def 1; :: thesis: verum