let L be complete Lattice; :: thesis: for a being Element of L holds
( a [= a *' & *' a [= a )
let a be Element of L; :: thesis: ( a [= a *' & *' a [= a )
set X = { d where d is Element of L : ( a [= d & d <> a ) } ;
A1: a is_less_than { d where d is Element of L : ( a [= d & d <> a ) }

proof

for q being Element of L st q in { d where d is Element of L : ( a [= d & d <> a ) } holds
a [= q

proof

let q be Element of L; :: thesis: ( q in { d where d is Element of L : ( a [= d & d <> a ) } implies a [= q )
assume q in { d where d is Element of L : ( a [= d & d <> a ) } ; :: thesis: a [= q
then ex q' being Element of L st
( q' = q & a [= q' & q' <> a ) ;
hence a [= q ; :: thesis: verum

end;

hence a is_less_than { d where d is Element of L : ( a [= d & d <> a ) } by LATTICE3:def 16; :: thesis: verum

end;

set X = { d where d is Element of L : ( d [= a & d <> a ) } ;
{ d where d is Element of L : ( d [= a & d <> a ) } is_less_than a

proof

for q being Element of L st q in { d where d is Element of L : ( d [= a & d <> a ) } holds
q [= a

proof

let q be Element of L; :: thesis: ( q in { d where d is Element of L : ( d [= a & d <> a ) } implies q [= a )
assume q in { d where d is Element of L : ( d [= a & d <> a ) } ; :: thesis: q [= a
then ex q' being Element of L st
( q' = q & q' [= a & q' <> a ) ;
hence q [= a ; :: thesis: verum

end;

hence { d where d is Element of L : ( d [= a & d <> a ) } is_less_than a by LATTICE3:def 17; :: thesis: verum

end;

hence ( a [= a *' & *' a [= a ) by A1, LATTICE3:34, LATTICE3:def 21; :: thesis: verum