theorem :: FILEREC1:25

for D being non empty set
for f, CR being File of D holds addcr (f,CR) is_preposition_of