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

proof

let p, q be Element of L; :: thesis: ( p [= q & p in PseudoCocomplements a implies q in PseudoCocomplements a )
assume C0: ( p [= q & p in PseudoCocomplements a ) ; :: thesis: q in PseudoCocomplements a
then consider x1 being Element of L such that
C1: ( x1 = p & a "\/" x1 = Top L ) ;
a "\/" p [= a "\/" q by C0, FILTER_0:1;
hence q in PseudoCocomplements a by C1; :: thesis: verum

end;

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

proof

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

end;

a "\/" (Top L) = Top L ;
then Top L in PseudoCocomplements a ;
hence ( PseudoCocomplements a is final & not PseudoCocomplements a is empty & PseudoCocomplements a is meet-closed ) by CC, C2; :: thesis: verum