theorem Th13: :: WAYBEL10:13

for L being reflexive RelStr
for S1, S2 being full SubRelStr of L st the carrier of S1 c= the carrier of S2 holds
S1 is SubRelStr of S2