set L = LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #);

for x, y, z being Element of LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

for x, y, z being Element of LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

proof

hence
LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is distributive
by LATTICES:def 11; :: thesis: verum
let x, y, z be Element of LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #); :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

reconsider xx = x, yy = y, zz = z as Element of T ;

R1: y "\/" z = Tern (yy,p,zz) by JoinDef;

R2: x "/\" y = Tern (xx,(p `),yy) by MeetDef;

R3: x "/\" z = Tern (xx,(p `),zz) by MeetDef;

reconsider xxzz = x "/\" z as Element of T ;

reconsider xxyy = x "/\" y as Element of T ;

reconsider yyzz = y "\/" z as Element of T ;

x "/\" (y "\/" z) = Tern (xx,(p `),yyzz) by MeetDef

.= Tern ((Tern (xx,(p `),yy)),p,(Tern (xx,(p `),zz))) by TDis, R1

.= the L_join of LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) . (xxyy,xxzz) by R2, R3, JoinDef ;

hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) ; :: thesis: verum

end;reconsider xx = x, yy = y, zz = z as Element of T ;

R1: y "\/" z = Tern (yy,p,zz) by JoinDef;

R2: x "/\" y = Tern (xx,(p `),yy) by MeetDef;

R3: x "/\" z = Tern (xx,(p `),zz) by MeetDef;

reconsider xxzz = x "/\" z as Element of T ;

reconsider xxyy = x "/\" y as Element of T ;

reconsider yyzz = y "\/" z as Element of T ;

x "/\" (y "\/" z) = Tern (xx,(p `),yyzz) by MeetDef

.= Tern ((Tern (xx,(p `),yy)),p,(Tern (xx,(p `),zz))) by TDis, R1

.= the L_join of LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) . (xxyy,xxzz) by R2, R3, JoinDef ;

hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) ; :: thesis: verum