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