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

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

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

proof

let x, y be Element of ; :: 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 A2, Th1;
hence y in Y by A1, WAYBEL_0:def 19; :: thesis: verum

end;

hence x is upper Subset of ; :: thesis: verum

end;

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

proof

let x, y be Element of ; :: 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 A4, LATTICE3:9;
hence y in Y by A3, WAYBEL_0:def 20; :: thesis: verum

end;

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