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 )

proof

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;

assume A2: for b being Element of B st b in { (b `) where b is Element of B : b in X } holds
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