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