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 b1 in { (x "/\" b2) where s is Element of S : b2 in {y,z} } ) )
hereby :: thesis: ( ( t = x "/\" y or t = x "/\" z ) implies b1 in { (x "/\" b2) where s is Element of S : b2 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: b1 in { (x "/\" b2) where s is Element of S : b2 in {y,z} }
per cases ( t = x "/\" y or t = x "/\" z ) by A3;
suppose A4: t = x "/\" y ; :: thesis: b1 in { (x "/\" b2) where s is Element of S : b2 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: b1 in { (x "/\" b2) where s is Element of S : b2 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