A1: RelStr(# the carrier of (L ~ ),the InternalRel of (L ~ ) #) = RelStr(# the carrier of (L opp+id ),the InternalRel of (L opp+id ) #) by Th11;
reconsider A = L ~ as with_suprema RelStr by YELLOW_7:16;
[#] A = [#] (L opp+id ) by Def6;
hence [#] (L opp+id ) is directed by A1, WAYBEL_0:3; :: according to WAYBEL_0:def 6 :: thesis: verum