let T be non empty TopSpace; :: thesis: for p being Point of T
for x, y being Element of (OpenNeighborhoods p) holds
( x <= y iff y c= x )
let p be Point of T; :: thesis: for x, y being Element of (OpenNeighborhoods p) holds
( x <= y iff y c= x )
set X = { V where V is Subset of T : ( p in V & V is open ) } ;
[#] T in { V where V is Subset of T : ( p in V & V is open ) } ;
then reconsider X = { V where V is Subset of T : ( p in V & V is open ) } as non empty set ;
let x, y be Element of (OpenNeighborhoods p); :: thesis: ( x <= y iff y c= x )
(InclPoset X) ~ = RelStr(# the carrier of (InclPoset X),( the InternalRel of (InclPoset X) ~) #) by LATTICE3:def 5;
then reconsider a = x, b = y as Element of (InclPoset X) ;
A1: ( b <= a iff y c= x ) by YELLOW_1:3;
( x = a ~ & y = b ~ ) by LATTICE3:def 6;
hence ( x <= y iff y c= x ) by A1, LATTICE3:9; :: thesis: verum