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)) #);
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)
;
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; verum