set X = the non empty finite set ;
set C = the Subset of the non empty finite set ;
set R = the Relation of the non empty finite set , the Subset of the non empty finite set ;
take D = ConstructorDB(# the non empty finite set , the Subset of the non empty finite set , the Relation of the non empty finite set , the Subset of the non empty finite set #); :: thesis: ( D is finite & not D is empty )
thus ( the carrier of D is finite & not the carrier of D is empty ) ; :: according to STRUCT_0:def 1,STRUCT_0:def 11 :: thesis: verum