theorem Th15: :: WAYBEL10:15

for L, R being RelStr
for x, y being Element of (Sub L) st y = R holds
( x <= y iff x is SubRelStr of R )