let X be ConstructorDB ; :: thesis: ( X is finite implies X is ref-finite )
assume A1: the carrier of X is finite ; :: according to STRUCT_0:def 11 :: thesis: X is ref-finite
let x be Element of X; :: according to MMLQUERY:def 30 :: thesis: x ref is finite
thus x ref is finite by A1; :: thesis: verum