set I0 = PseudoComplements a;
CC: for p, q being Element of L st p [= q & q in PseudoComplements a holds
p in PseudoComplements a

proof

let p, q be Element of L; :: thesis: ( p [= q & q in PseudoComplements a implies p in PseudoComplements a )
assume C0: ( p [= q & q in PseudoComplements a ) ; :: thesis: p in PseudoComplements a
then consider x1 being Element of L such that
C1: ( x1 = q & a "/\" x1 = Bottom L ) ;
C2: Bottom L [= a "/\" p ;
a "/\" p [= a "/\" q by C0, LATTICES:9;
then a "/\" p = Bottom L by C2, LATTICES:8, C1;
hence p in PseudoComplements a ; :: thesis: verum

end;

C2: for p, q being Element of L st p in PseudoComplements a & q in PseudoComplements a holds
p "\/" q in PseudoComplements a

proof

let p, q be Element of L; :: thesis: ( p in PseudoComplements a & q in PseudoComplements a implies p "\/" q in PseudoComplements a )
assume d0: ( p in PseudoComplements a & q in PseudoComplements a ) ; :: thesis: p "\/" q in PseudoComplements a
then consider x1 being Element of L such that
d1: ( x1 = p & a "/\" x1 = Bottom L ) ;
consider x2 being Element of L such that
d2: ( x2 = q & a "/\" x2 = Bottom L ) by d0;
a "/\" (x1 "\/" x2) = (a "/\" x1) "\/" (a "/\" x2) by LATTICES:def 11
.= Bottom L by d1, d2 ;
hence p "\/" q in PseudoComplements a by d1, d2; :: thesis: verum

end;

a "/\" (Bottom L) = Bottom L ;
then Bottom L in PseudoComplements a ;
hence ( PseudoComplements a is initial & not PseudoComplements a is empty & PseudoComplements a is join-closed ) by CC, C2; :: thesis: verum