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 )

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

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