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)
proof
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
.= 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 ;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) ; :: thesis: verum
end;
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