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 :: thesis: for X being set
for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C)
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, Th51;
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:9;
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 7;
hence a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C) by A3, LATTICES:7; :: thesis: verum
end;
hence C is \/-distributive by Th33; :: thesis: verum