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