theorem Th24: :: FILEREC1:24

for D being non empty set
for f, CR being File of D holds f is_preposition_of f ^ CR