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 ex c being Element of B st
( b = c ` & c in X ) ;
hence b [= a ` 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
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 A3: b ` in { (b `) where b is Element of B : b in X } ;
A4: (a `) ` = a ;
(b `) ` = b ;
hence a [= b by A2, A3, A4, LATTICES:26; :: thesis: verum