RelStr(# the carrier of (L ~), the InternalRel of (L ~) #) = RelStr(# the carrier of (L opp+id), the InternalRel of (L opp+id) #) by Th11;
hence not L opp+id is empty ; :: thesis: verum