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 ; :: 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:
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 ; :: thesis: verum