theorem :: YELLOW_7:3

for L being RelStr holds
( L is empty iff L opp is empty ) ;