let X be set ; :: thesis: for B being B_Lattice
for a being Element of B holds
( X is_greater_than a iff { (b ` ) where b is Element of B : b in X } is_less_than a ` )
let B be B_Lattice; :: thesis: for a being Element of B holds
( X is_greater_than a iff { (b ` ) where b is Element of B : b in X } is_less_than a ` )
let a be Element of B; :: thesis: ( X is_greater_than a iff { (b ` ) where b is Element of B : b in X } is_less_than a ` )
set Y = { (b ` ) where b is Element of B : b in X } ;
thus ( X is_greater_than a implies { (b ` ) where b is Element of B : b in X } is_less_than a ` ) :: thesis: ( { (b ` ) where b is Element of B : b in X } is_less_than a ` implies X is_greater_than a )

proof

assume A1: for b being Element of B st b in X holds
a [= b ; :: according to LATTICE3:def 16 :: thesis: { (b ` ) where b is Element of B : b in X } is_less_than a `
let b be Element of B; :: according to LATTICE3:def 17 :: thesis: ( b in { (b ` ) where b is Element of B : b in X } implies b [= a ` )
assume b in { (b ` ) where b is Element of B : b in X } ; :: thesis: b [= a `
then consider c being Element of B such that
A2: ( b = c ` & c in X ) ;
thus b [= a ` 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
b [= a ` ; :: according to LATTICE3:def 17 :: thesis: X is_greater_than a
let b be Element of B; :: according to LATTICE3:def 16 :: thesis: ( b in X implies a [= b )
assume b in X ; :: thesis: a [= b
then b ` in { (b ` ) where b is Element of B : b in X } ;
then ( b ` [= a ` & (a ` ) ` = a & (b ` ) ` = b ) by A3, LATTICES:49;
hence a [= b by LATTICES:53; :: thesis: verum