let C be complete Lattice; :: thesis: for a being Element of C holds
( a = "\/" ( { b where b is Element of C : b [= a } ,C) & a = "/\" ( { c where c is Element of C : a [= c } ,C) )
let a be Element of C; :: thesis: ( a = "\/" ( { b where b is Element of C : b [= a } ,C) & a = "/\" ( { c where c is Element of C : a [= c } ,C) )
set X = { b where b is Element of C : b [= a } ;
set Y = { c where c is Element of C : a [= c } ;
A1: a in { b where b is Element of C : b [= a } ;
A2: a in { c where c is Element of C : a [= c } ;
{ b where b is Element of C : b [= a } is_less_than a
proof
let b be Element of C; :: according to LATTICE3:def 17 :: thesis: ( b in { b where b is Element of C : b [= a } implies b [= a )
assume b in { b where b is Element of C : b [= a } ; :: thesis: b [= a
then ex c being Element of C st
( b = c & c [= a ) ;
hence b [= a ; :: thesis: verum
end;
hence a = "\/" ( { b where b is Element of C : b [= a } ,C) by A1, Th40; :: thesis: a = "/\" ( { c where c is Element of C : a [= c } ,C)
a is_less_than { c where c is Element of C : a [= c }
proof
let b be Element of C; :: according to LATTICE3:def 16 :: thesis: ( b in { c where c is Element of C : a [= c } implies a [= b )
assume b in { c where c is Element of C : a [= c } ; :: thesis: a [= b
then ex c being Element of C st
( b = c & a [= c ) ;
hence a [= b ; :: thesis: verum
end;
hence a = "/\" ( { c where c is Element of C : a [= c } ,C) by A2, Th41; :: thesis: verum