theorem Th25: :: YELLOW16:26

for L being RelStr
for S being full SubRelStr of L
for R being SubRelStr of S holds
( R is full iff R is full SubRelStr of L )