:: deftheorem Def1 defines incl YELLOW_9:def 1 :
for R, S being 1-sorted st the carrier of S c= the carrier of R holds
incl (S,R) = id the carrier of S;