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 )

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 )

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

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

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;
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;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

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

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;
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;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

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