:: deftheorem Def1 defines meet SETFAM_1:def 1 :
for X, b₂ being set holds
( ( X <> {} implies ( b₂ = meet X iff for x being object holds
( x in b₂ iff for Y being set st Y in X holds
x in Y ) ) ) & ( not X <> {} implies ( b₂ = meet X iff b₂ = {} ) ) );