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} } ;

now

let t be set ; :: 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 consider s being Element of S such that
A2: t = x "/\" s and
A3: s in {y,z} ;
thus ( t = x "/\" y or t = x "/\" z ) by A2, A3, TARSKI:def 2; :: thesis: verum

end;

assume A4: ( 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 A4;

suppose A5: 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 A5; :: thesis: verum

end;

suppose A6: 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 A6; :: thesis: verum

end;

end;

end;

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