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