let L be RelStr ; :: thesis: RelStr(# the carrier of (L ~ ),the InternalRel of (L ~ ) #) = RelStr(# the carrier of (L opp+id ),the InternalRel of (L opp+id ) #)
the InternalRel of (L ~ ) = the InternalRel of (L opp+id ) by Def6;
hence RelStr(# the carrier of (L ~ ),the InternalRel of (L ~ ) #) = RelStr(# the carrier of (L opp+id ),the InternalRel of (L opp+id ) #) by Def6; :: thesis: verum