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