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
proof
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)) #);
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;
verum
end;
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; verum