for L being RelStr
for X being Subset of L holds RelStr(# X,( the InternalRel of L |_2 X) #) is full SubRelStr of L by XBOOLE_1:17, Def13, Def14;