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_{1} being Element of the carrier of (BoolePoset ([#] T)) st

( b_{1} in NeighborhoodSystem x & b_{1} <= a & b_{1} <= b ) )

assume that

A4: a in NeighborhoodSystem x and

A5: b in NeighborhoodSystem x ; :: thesis: ex b_{1} being Element of the carrier of (BoolePoset ([#] T)) st

( b_{1} in NeighborhoodSystem x & b_{1} <= a & b_{1} <= 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

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 2 :: thesis: ( not a in NeighborhoodSystem x or not b in NeighborhoodSystem x or ex b
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;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

( b

assume that

A4: a in NeighborhoodSystem x and

A5: b in NeighborhoodSystem x ; :: thesis: ex 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