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:
{} 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:
thus NeighborhoodSystem x is upper :: thesis:

let a, b be Element of (BoolePoset ([#] T)); :: according to WAYBEL_0:def 20 :: thesis:
reconsider B = b as Subset of T by WAYBEL_7:2;
assume a in NeighborhoodSystem x ; :: thesis:
then reconsider A = a as a_neighborhood of x by Th2;
assume a <= b ; :: thesis:
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:

end;

let a, b be Element of (BoolePoset ([#] T)); :: according to WAYBEL_0:def 2 :: thesis:
assume that
A4: a in NeighborhoodSystem x and
A5: b in NeighborhoodSystem x ; :: thesis:
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:
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: