let X be set ; :: thesis: for B being B_Lattice

for a being Element of B holds

( X is_less_than a iff { (b `) where b is Element of B : b in X } is_greater_than a ` )

let B be B_Lattice; :: thesis: for a being Element of B holds

( X is_less_than a iff { (b `) where b is Element of B : b in X } is_greater_than a ` )

let a be Element of B; :: thesis: ( X is_less_than a iff { (b `) where b is Element of B : b in X } is_greater_than a ` )

set Y = { (b `) where b is Element of B : b in X } ;

thus ( X is_less_than a implies { (b `) where b is Element of B : b in X } is_greater_than a ` ) :: thesis: ( { (b `) where b is Element of B : b in X } is_greater_than a ` implies X is_less_than a )

a ` [= b ; :: according to LATTICE3:def 16 :: thesis: X is_less_than a

let b be Element of B; :: according to LATTICE3:def 17 :: thesis: ( b in X implies b [= a )

assume b in X ; :: thesis: b [= a

then A3: b ` in { (b `) where b is Element of B : b in X } ;

A4: (a `) ` = a ;

(b `) ` = b ;

hence b [= a by A2, A3, A4, LATTICES:26; :: thesis: verum

for a being Element of B holds

( X is_less_than a iff { (b `) where b is Element of B : b in X } is_greater_than a ` )

let B be B_Lattice; :: thesis: for a being Element of B holds

( X is_less_than a iff { (b `) where b is Element of B : b in X } is_greater_than a ` )

let a be Element of B; :: thesis: ( X is_less_than a iff { (b `) where b is Element of B : b in X } is_greater_than a ` )

set Y = { (b `) where b is Element of B : b in X } ;

thus ( X is_less_than a implies { (b `) where b is Element of B : b in X } is_greater_than a ` ) :: thesis: ( { (b `) where b is Element of B : b in X } is_greater_than a ` implies X is_less_than a )

proof

assume A2:
for b being Element of B st b in { (b `) where b is Element of B : b in X } holds
assume A1:
for b being Element of B st b in X holds

b [= a ; :: according to LATTICE3:def 17 :: thesis: { (b `) where b is Element of B : b in X } is_greater_than a `

let b be Element of B; :: according to LATTICE3:def 16 :: thesis: ( b in { (b `) where b is Element of B : b in X } implies a ` [= b )

assume b in { (b `) where b is Element of B : b in X } ; :: thesis: a ` [= b

then ex c being Element of B st

( b = c ` & c in X ) ;

hence a ` [= b by A1, LATTICES:26; :: thesis: verum

end;b [= a ; :: according to LATTICE3:def 17 :: thesis: { (b `) where b is Element of B : b in X } is_greater_than a `

let b be Element of B; :: according to LATTICE3:def 16 :: thesis: ( b in { (b `) where b is Element of B : b in X } implies a ` [= b )

assume b in { (b `) where b is Element of B : b in X } ; :: thesis: a ` [= b

then ex c being Element of B st

( b = c ` & c in X ) ;

hence a ` [= b by A1, LATTICES:26; :: thesis: verum

a ` [= b ; :: according to LATTICE3:def 16 :: thesis: X is_less_than a

let b be Element of B; :: according to LATTICE3:def 17 :: thesis: ( b in X implies b [= a )

assume b in X ; :: thesis: b [= a

then A3: b ` in { (b `) where b is Element of B : b in X } ;

A4: (a `) ` = a ;

(b `) ` = b ;

hence b [= a by A2, A3, A4, LATTICES:26; :: thesis: verum