consider A0 being a_neighborhood of x;
A0 in NeighborhoodSystem x ;
hence not NeighborhoodSystem x is empty ; :: thesis: ( NeighborhoodSystem x is proper & NeighborhoodSystem x is upper & NeighborhoodSystem x is filtered )
set X = the carrier of T;
set L = BoolePoset ([#] T);
set Y = NeighborhoodSystem x;
A1: the carrier of (BoolePoset the carrier of T) = bool the carrier of T by WAYBEL_7:4;
A3: {} is not a_neighborhood of x by CONNSP_2:6;
{} c= the carrier of T by XBOOLE_1:2;
then ( {} in bool the carrier of T & not {} in NeighborhoodSystem x ) by A3, Th3;
hence NeighborhoodSystem x is proper by A1, SUBSET_1:def 7; :: 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 )
assume a in NeighborhoodSystem x ; :: thesis: ( not a <= b or b in NeighborhoodSystem x )
then reconsider A = a as a_neighborhood of x by Th3;
reconsider B = b as Subset of T by WAYBEL_7:4;
assume a <= b ; :: thesis: b in NeighborhoodSystem x
then A c= B by YELLOW_1:2;
then ( Int A c= Int B & x in Int A ) by CONNSP_2:def 1, TOPS_1:48;
then b is a_neighborhood of x by 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 ( a in NeighborhoodSystem x & b in NeighborhoodSystem x ) ; :: thesis: ex b₁ being Element of the carrier of (BoolePoset ([#] T)) st
( b₁ in NeighborhoodSystem x & b₁ <= a & b₁ <= b )
then reconsider A = a, B = b as a_neighborhood of x by Th3;
A4: A /\ B is a_neighborhood of x by CONNSP_2:4;
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 )
( z c= A & z c= B ) by XBOOLE_1:17;
hence ( z in NeighborhoodSystem x & z <= a & z <= b ) by A4, YELLOW_1:2; :: thesis: verum