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

hereby :: thesis: ( x is upper Subset of (L opp ) implies x is lower Subset of L )

assume x is lower Subset of L ; :: thesis: x is upper Subset of (L opp )
then reconsider X = x as lower Subset of L ;
reconsider Y = X as Subset of (L opp ) ;
Y is upper

proof

let x, y be Element of (L opp ); :: according to WAYBEL_0:def 20 :: thesis: ( not x in Y or not x <= y or y in Y )
assume A1: ( x in Y & x <= y ) ; :: thesis: y in Y
then ( x = ~ x & y = ~ y & ~ x >= ~ y ) by Th1;
hence y in Y by A1, WAYBEL_0:def 19; :: thesis: verum

end;

hence x is upper Subset of (L opp ) ; :: thesis: verum

end;

assume x is upper Subset of (L opp ) ; :: thesis: x is lower Subset of L
then reconsider X = x as upper Subset of (L opp ) ;
reconsider Y = X as Subset of L ;
Y is lower

proof

let x, y be Element of L; :: according to WAYBEL_0:def 19 :: thesis: ( not x in Y or not y <= x or y in Y )
assume A2: ( x in Y & x >= y ) ; :: thesis: y in Y
then ( x = x ~ & y = y ~ & x ~ <= y ~ ) by LATTICE3:9;
hence y in Y by A2, WAYBEL_0:def 20; :: thesis: verum

end;

hence x is lower Subset of L ; :: thesis: verum