set L = LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #);

for b being Element of LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) ex 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)) #) st a is_a_complement_of b

for b being Element of LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) ex 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)) #) st a is_a_complement_of b

proof

hence
LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is complemented
by LATTICES:def 19; :: thesis: verum
let b 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: ex 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)) #) st a is_a_complement_of b

reconsider bb = b as Element of T ;

reconsider aa = bb ` as Element of T ;

reconsider a = aa as Element of LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) ;

A1: a "/\" b = Tern (aa,(p `),bb) by MeetDef

.= Tern ((bb `),bb,(p `)) by Th36a

.= p ` by TLADef

.= Bottom LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) by BotTBA ;

a "\/" b = Tern (aa,p,bb) by JoinDef

.= Tern ((bb `),bb,p) by Th36a

.= p by TLADef

.= Top LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) by TopTBA ;

hence ex 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)) #) st a is_a_complement_of b by A1, LATTICES:def 18; :: thesis: verum

end;reconsider bb = b as Element of T ;

reconsider aa = bb ` as Element of T ;

reconsider a = aa as Element of LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) ;

A1: a "/\" b = Tern (aa,(p `),bb) by MeetDef

.= Tern ((bb `),bb,(p `)) by Th36a

.= p ` by TLADef

.= Bottom LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) by BotTBA ;

a "\/" b = Tern (aa,p,bb) by JoinDef

.= Tern ((bb `),bb,p) by Th36a

.= p by TLADef

.= Top LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) by TopTBA ;

hence ex 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)) #) st a is_a_complement_of b by A1, LATTICES:def 18; :: thesis: verum