let C be complete Lattice; :: thesis: ( C is I_Lattice implies C is \/-distributive )
assume A1: C is I_Lattice ; :: thesis: C is \/-distributive

now

let X be set ; :: thesis: for a being Element of C holds a "/\" ("\/" X,C) [= "\/" { (a "/\" a9) where a9 is Element of C : a9 in X } ,C
let a be Element of C; :: thesis: a "/\" ("\/" X,C) [= "\/" { (a "/\" a9) where a9 is Element of C : a9 in X } ,C
set Y = { (a "/\" a9) where a9 is Element of C : a9 in X } ;
set b = "\/" X,C;
set c = "\/" { (a "/\" a9) where a9 is Element of C : a9 in X } ,C;
set Z = { b9 where b9 is Element of C : a "/\" b9 [= "\/" { (a "/\" a9) where a9 is Element of C : a9 in X } ,C } ;
X is_less_than a => ("\/" { (a "/\" a9) where a9 is Element of C : a9 in X } ,C)

proof

let b9 be Element of C; :: according to LATTICE3:def 17 :: thesis: ( b9 in X implies b9 [= a => ("\/" { (a "/\" a9) where a9 is Element of C : a9 in X } ,C) )
assume b9 in X ; :: thesis: b9 [= a => ("\/" { (a "/\" a9) where a9 is Element of C : a9 in X } ,C)
then a "/\" b9 in { (a "/\" a9) where a9 is Element of C : a9 in X } ;
then a "/\" b9 [= "\/" { (a "/\" a9) where a9 is Element of C : a9 in X } ,C by Th38;
then A2: b9 in { b9 where b9 is Element of C : a "/\" b9 [= "\/" { (a "/\" a9) where a9 is Element of C : a9 in X } ,C } ;
a => ("\/" { (a "/\" a9) where a9 is Element of C : a9 in X } ,C) = "\/" { b9 where b9 is Element of C : a "/\" b9 [= "\/" { (a "/\" a9) where a9 is Element of C : a9 in X } ,C } ,C by A1, Th52;
hence b9 [= a => ("\/" { (a "/\" a9) where a9 is Element of C : a9 in X } ,C) by A2, Th38; :: thesis: verum

end;

then "\/" X,C [= a => ("\/" { (a "/\" a9) where a9 is Element of C : a9 in X } ,C) by Def21;
then A3: a "/\" ("\/" X,C) [= a "/\" (a => ("\/" { (a "/\" a9) where a9 is Element of C : a9 in X } ,C)) by LATTICES:27;
a "/\" (a => ("\/" { (a "/\" a9) where a9 is Element of C : a9 in X } ,C)) [= "\/" { (a "/\" a9) where a9 is Element of C : a9 in X } ,C by A1, FILTER_0:def 8;
hence a "/\" ("\/" X,C) [= "\/" { (a "/\" a9) where a9 is Element of C : a9 in X } ,C by A3, LATTICES:25; :: thesis: verum

end;

hence C is \/-distributive by Th33; :: thesis: verum