set Y = NeighborhoodSystem x;
set X = the carrier of T;
set L = BoolePoset ([#] T);
set A0 = the a_neighborhood of x;
the a_neighborhood of x in NeighborhoodSystem x ;
hence not NeighborhoodSystem x is empty ; :: thesis: ( NeighborhoodSystem x is proper & NeighborhoodSystem x is upper & NeighborhoodSystem x is filtered )
{} c= the carrier of T ;
then A1: {} in bool the carrier of T ;
{} is not a_neighborhood of x by CONNSP_2:4;
then A2: not {} in NeighborhoodSystem x by Th2;
the carrier of (BoolePoset the carrier of T) = bool the carrier of T by WAYBEL_7:2;
hence NeighborhoodSystem x is proper by A1, A2; :: thesis: ( NeighborhoodSystem x is upper & NeighborhoodSystem x is filtered )
thus NeighborhoodSystem x is upper :: thesis: NeighborhoodSystem x is filtered

proof

let a, b be Element of (BoolePoset ([#] T)); :: according to WAYBEL_0:def 20 :: thesis: ( not a in NeighborhoodSystem x or not a <= b or b in NeighborhoodSystem x )
reconsider B = b as Subset of T by WAYBEL_7:2;
assume a in NeighborhoodSystem x ; :: thesis: ( not a <= b or b in NeighborhoodSystem x )
then reconsider A = a as a_neighborhood of x by Th2;
assume a <= b ; :: thesis: b in NeighborhoodSystem x
then A c= B by YELLOW_1:2;
then A3: Int A c= Int B by TOPS_1:19;
x in Int A by CONNSP_2:def 1;
then b is a_neighborhood of x by A3, CONNSP_2:def 1;
hence b in NeighborhoodSystem x ; :: thesis: verum

end;

let a, b be Element of (BoolePoset ([#] T)); :: according to WAYBEL_0:def 2 :: thesis: ( not a in NeighborhoodSystem x or not b in NeighborhoodSystem x or ex b₁ being Element of the carrier of (BoolePoset ([#] T)) st
( b₁ in NeighborhoodSystem x & b₁ <= a & b₁ <= b ) )
assume that
A4: a in NeighborhoodSystem x and
A5: b in NeighborhoodSystem x ; :: thesis: ex b₁ being Element of the carrier of (BoolePoset ([#] T)) st
( b₁ in NeighborhoodSystem x & b₁ <= a & b₁ <= b )
reconsider A = a, B = b as a_neighborhood of x by A4, A5, Th2;
A6: A /\ B is a_neighborhood of x by CONNSP_2:2;
then A /\ B in NeighborhoodSystem x ;
then reconsider z = A /\ B as Element of (BoolePoset ([#] T)) ;
take z ; :: thesis: ( z in NeighborhoodSystem x & z <= a & z <= b )
A7: z c= B by XBOOLE_1:17;
z c= A by XBOOLE_1:17;
hence ( z in NeighborhoodSystem x & z <= a & z <= b ) by A6, A7, YELLOW_1:2; :: thesis: verum