set L = LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #);
ex c being Element of LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) st
for a 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
( c "/\" a = c & a "/\" c = c )
proof
reconsider pp =
p as
Element of
LattStr(# the
carrier of
(TBA2BA (T,p)), the
L_join of
(TBA2BA (T,p)), the
L_meet of
(TBA2BA (T,p)) #) ;
reconsider t =
p ` as
Element of
LattStr(# the
carrier of
(TBA2BA (T,p)), the
L_join of
(TBA2BA (T,p)), the
L_meet of
(TBA2BA (T,p)) #) ;
take
t
;
for a 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
( t "/\" a = t & a "/\" t = t )
reconsider tt =
t as
Element of
T ;
let a be
Element of
LattStr(# the
carrier of
(TBA2BA (T,p)), the
L_join of
(TBA2BA (T,p)), the
L_meet of
(TBA2BA (T,p)) #);
( t "/\" a = t & a "/\" t = t )
reconsider aa =
a as
Element of
T ;
a "/\" t =
Tern (
aa,
(p `),
tt)
by MeetDef
.=
tt
by TRIDef
;
hence
(
t "/\" a = t &
a "/\" t = t )
;
verum
end;
then A1:
LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is lower-bounded
by LATTICES:def 13;
ex c being Element of LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) st
for a 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
( c "\/" a = c & a "\/" c = c )
proof
reconsider pp =
p as
Element of
LattStr(# the
carrier of
(TBA2BA (T,p)), the
L_join of
(TBA2BA (T,p)), the
L_meet of
(TBA2BA (T,p)) #) ;
take t =
pp;
for a 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
( t "\/" a = t & a "\/" t = t )
reconsider tt =
t as
Element of
T ;
let a be
Element of
LattStr(# the
carrier of
(TBA2BA (T,p)), the
L_join of
(TBA2BA (T,p)), the
L_meet of
(TBA2BA (T,p)) #);
( t "\/" a = t & a "\/" t = t )
reconsider aa =
a as
Element of
T ;
t "\/" a =
Tern (
tt,
p,
aa)
by JoinDef
.=
tt
by TLIDef
;
hence
(
t "\/" a = t &
a "\/" t = t )
;
verum
end;
then
LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is upper-bounded
by LATTICES:def 14;
hence
LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is bounded
by A1; verum