let C be complete Lattice; :: thesis: for a, b being Element of C st C is I_Lattice holds
a => b = "\/" ( { c where c is Element of C : a "/\" c [= b } ,C)
let a, b be Element of C; :: thesis: ( C is I_Lattice implies a => b = "\/" ( { c where c is Element of C : a "/\" c [= b } ,C) )
set X = { a9 where a9 is Element of C : a "/\" a9 [= b } ;
assume A1: C is I_Lattice ; :: thesis: a => b = "\/" ( { c where c is Element of C : a "/\" c [= b } ,C)
then a "/\" (a => b) [= b by FILTER_0:def 7;
then A2: a => b in { a9 where a9 is Element of C : a "/\" a9 [= b } ;
{ a9 where a9 is Element of C : a "/\" a9 [= b } is_less_than a => b

proof

let c be Element of C; :: according to LATTICE3:def 17 :: thesis: ( c in { a9 where a9 is Element of C : a "/\" a9 [= b } implies c [= a => b )
assume c in { a9 where a9 is Element of C : a "/\" a9 [= b } ; :: thesis: c [= a => b
then ex a9 being Element of C st
( c = a9 & a "/\" a9 [= b ) ;
hence c [= a => b by A1, FILTER_0:def 7; :: thesis: verum

end;

hence a => b = "\/" ( { c where c is Element of C : a "/\" c [= b } ,C) by A2, Th40; :: thesis: verum