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