let L be RelStr ; :: thesis: for x being set holds

( x is lower Subset of (L opp) iff x is upper Subset of L )

let x be set ; :: thesis: ( x is lower Subset of (L opp) iff x is upper Subset of L )

( x is upper Subset of L iff x is upper Subset of ((L opp) ~) ) by WAYBEL_0:25;

hence ( x is lower Subset of (L opp) iff x is upper Subset of L ) by Th28; :: thesis: verum

( x is lower Subset of (L opp) iff x is upper Subset of L )

let x be set ; :: thesis: ( x is lower Subset of (L opp) iff x is upper Subset of L )

( x is upper Subset of L iff x is upper Subset of ((L opp) ~) ) by WAYBEL_0:25;

hence ( x is lower Subset of (L opp) iff x is upper Subset of L ) by Th28; :: thesis: verum