theorem :: FILEREC1:25

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