:: deftheorem Def14 defines full YELLOW_0:def 14 :
for L being RelStr
for S being SubRelStr of L holds
( S is full iff the InternalRel of S = the InternalRel of L |_2 the carrier of S );