theorem Th28: :: YELLOW_7:28

for L being RelStr
for x being set holds
( x is lower Subset of L iff x is upper Subset of (L opp) )