let T be non empty TopSpace; :: thesis: for p being Point of
for x, y being Element of holds
( x <= y iff y c= x )
let p be Point of ; :: thesis: for x, y being Element of holds
( x <= y iff y c= x )
set X = { V where V is Subset of : ( p in V & V is open ) } ;
[#] T is open by TOPS_1:53;
then [#] T in { V where V is Subset of : ( p in V & V is open ) } ;
then reconsider X = { V where V is Subset of : ( p in V & V is open ) } as non empty set ;
let x, y be Element of ; :: 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 ;
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