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 ) } ;
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 q9 being Element of L st
( q9 = q & a [= q9 & q9 <> a ) ;
hence a [= q ; :: thesis: verum
end;
then A1: a is_less_than { d where d is Element of L : ( a [= d & d <> a ) } by LATTICE3:def 16;
set X = { d where d is Element of L : ( d [= a & d <> a ) } ;
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 q9 being Element of L st
( q9 = q & q9 [= a & q9 <> a ) ;
hence q [= a ; :: thesis: verum
end;
then { d where d is Element of L : ( d [= a & d <> a ) } is_less_than a by LATTICE3:def 17;
hence ( a [= a *' & *' a [= a ) by A1, LATTICE3:34, LATTICE3:def 21; :: thesis: verum