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

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