let S be LATTICE; :: thesis: ( ( for X being Subset of S st ex_sup_of X,S holds
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) implies S is distributive )
assume A1: for X being Subset of S st ex_sup_of X,S holds
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ; :: thesis: S is distributive
let x, y, z be Element of S; :: according to WAYBEL_1:def 3 :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
set Y = { (x "/\" s) where s is Element of S : s in {y,z} } ;
A2: ex_sup_of {y,z},S by YELLOW_0:20;

now :: thesis: for t being object holds
( ( not t in { (x "/\" s) where s is Element of S : s in {y,z} } or t = x "/\" y or t = x "/\" z ) & ( ( t = x "/\" y or t = x "/\" z ) implies t in { (x "/\" s) where s is Element of S : s in {y,z} } ) )

let t be object ; :: thesis: ( ( not t in { (x "/\" s) where s is Element of S : s in {y,z} } or t = x "/\" y or t = x "/\" z ) & ( ( t = x "/\" y or t = x "/\" z ) implies b₁ in { (x "/\" b₂) where s is Element of S : b₂ in {y,z} } ) )

hereby :: thesis: ( ( t = x "/\" y or t = x "/\" z ) implies b₁ in { (x "/\" b₂) where s is Element of S : b₂ in {y,z} } )

assume t in { (x "/\" s) where s is Element of S : s in {y,z} } ; :: thesis: ( t = x "/\" y or t = x "/\" z )
then ex s being Element of S st
( t = x "/\" s & s in {y,z} ) ;
hence ( t = x "/\" y or t = x "/\" z ) by TARSKI:def 2; :: thesis: verum

end;

assume A3: ( t = x "/\" y or t = x "/\" z ) ; :: thesis: b₁ in { (x "/\" b₂) where s is Element of S : b₂ in {y,z} }

per cases ( t = x "/\" y or t = x "/\" z ) by A3;

suppose A4: t = x "/\" y ; :: thesis: b₁ in { (x "/\" b₂) where s is Element of S : b₂ in {y,z} }

y in {y,z} by TARSKI:def 2;
hence t in { (x "/\" s) where s is Element of S : s in {y,z} } by A4; :: thesis: verum

end;

suppose A5: t = x "/\" z ; :: thesis: b₁ in { (x "/\" b₂) where s is Element of S : b₂ in {y,z} }

z in {y,z} by TARSKI:def 2;
hence t in { (x "/\" s) where s is Element of S : s in {y,z} } by A5; :: thesis: verum

end;

end;

end;

then A6: { (x "/\" s) where s is Element of S : s in {y,z} } = {(x "/\" y),(x "/\" z)} by TARSKI:def 2;
thus x "/\" (y "\/" z) = x "/\" (sup {y,z}) by YELLOW_0:41
.= "\/" ({(x "/\" y),(x "/\" z)},S) by A1, A6, A2
.= (x "/\" y) "\/" (x "/\" z) by YELLOW_0:41 ; :: thesis: verum