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 holds a "/\" ("\/" X,C) [= "\/" { (a "/\" a') where a' is Element of : a' in X } ,C
let a be Element of ; :: thesis: a "/\" ("\/" X,C) [= "\/" { (a "/\" a') where a' is Element of : a' in X } ,C
set Y = { (a "/\" a') where a' is Element of : a' in X } ;
set b = "\/" X,C;
set c = "\/" { (a "/\" a') where a' is Element of : a' in X } ,C;
set Z = { b' where b' is Element of : a "/\" b' [= "\/" { (a "/\" a') where a' is Element of : a' in X } ,C } ;
X is_less_than a => ("\/" { (a "/\" a') where a' is Element of : a' in X } ,C)

proof

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

end;

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

end;

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