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 = { a' where a' is Element of C : a "/\" a' [= 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 8;
then A2: a => b in { a' where a' is Element of C : a "/\" a' [= b } ;
{ a' where a' is Element of C : a "/\" a' [= b } is_less_than a => b

proof

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

end;

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