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 that
A1: x in Y and
A2: x <= y ; :: thesis: y in Y
~ x >= ~ y by ;
hence y in Y by ; :: 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 that
A3: x in Y and
A4: x >= y ; :: thesis: y in Y
x ~ <= y ~ by ;
hence y in Y by ; :: thesis: verum
end;
hence x is lower Subset of L ; :: thesis: verum