dom (Start-At (k,S)) misses NAT by Th26;
hence (Start-At (k,S)) | NAT = {} by RELAT_1:95; :: according to COMPOS_1:def 29 :: thesis: verum