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) )

then reconsider X = x as upper Subset of (L opp) ;

reconsider Y = X as Subset of L ;

Y is lower

( 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 upper Subset of (L opp)
; :: thesis: x is lower Subset of Lassume
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

end;then reconsider X = x as lower Subset of L ;

reconsider Y = X as Subset of (L opp) ;

Y is upper

proof

hence
x is upper Subset of (L opp)
; :: thesis: verum
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 A2, Th1;

hence y in Y by A1, WAYBEL_0:def 19; :: thesis: verum

end;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

then reconsider X = x as upper Subset of (L opp) ;

reconsider Y = X as Subset of L ;

Y is lower

proof

hence
x is lower Subset of L
; :: thesis: verum
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 A4, LATTICE3:9;

hence y in Y by A3, WAYBEL_0:def 20; :: thesis: verum

end;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