:: deftheorem defines <- MMLQUER2:def 8 :
for A being FinSequence
for x being object holds A <- x = meet (A " {x});