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 consider c being Element of B such that
A2: ( b = c ` & c in X ) ;
thus a ` [= b by A1, A2, LATTICES:53; :: thesis: verum

end;

assume A3: 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 b ` in { (b ` ) where b is Element of B : b in X } ;
then ( a ` [= b ` & (a ` ) ` = a & (b ` ) ` = b ) by A3, LATTICES:49;
hence b [= a by LATTICES:53; :: thesis: verum