reconsider n = n as Element of NAT by ORDINAL1:def 12;
f . n is Element of bool [:X,X:] ;
hence f . n is Relation-like ; :: thesis: verum