:: deftheorem Def6 defines LBound CARD_LAR:def 6 :
for A being limit_ordinal infinite Ordinal
for X being Subset of A
for B1 being Ordinal st X is unbounded & B1 in A holds
LBound (B1,X) = inf { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } ;