let T be Ternary_Boolean_Algebra; :: thesis: for p being Element of T holds Top LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) = p
let p be Element of T; :: thesis: Top LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) = p
set L = 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)) #) ;
reconsider tt = t as Element of 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 )

proof

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 JoinDef
.= tt by TRIDef ;
hence ( t "\/" a = t & a "\/" t = t ) ; :: thesis: verum

end;

hence Top LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) = p by LATTICES:def 17; :: thesis: verum