let L be complete Scott TopLattice; :: thesis: for x being Element of L
for X being Subset of L st X is open & x in X holds
inf X << x
let x be Element of L; :: thesis: for X being Subset of L st X is open & x in X holds
inf X << x
let X be Subset of L; :: thesis: ( X is open & x in X implies inf X << x )
assume that
A1: X is open and
A2: x in X ; :: thesis: inf X << x
A3: ( X is upper & X is property(S) ) by A1, WAYBEL11:15;
now :: thesis: for D being non empty directed Subset of L st x <= sup D holds
ex y being Element of L st
( y in D & inf X <= y )
let D be non empty directed Subset of L; :: thesis: ( x <= sup D implies ex y being Element of L st
( y in D & inf X <= y ) )
assume x <= sup D ; :: thesis: ex y being Element of L st
( y in D & inf X <= y )
then sup D in X by A2, A3;
then consider y being Element of L such that
A4: y in D and
A5: for x being Element of L st x in D & x >= y holds
x in X by A3, WAYBEL11:def 3;
take y = y; :: thesis: ( y in D & inf X <= y )
thus y in D by A4; :: thesis: inf X <= y
y <= y ;
then ( inf X is_<=_than X & y in X ) by A4, A5, YELLOW_0:33;
hence inf X <= y by LATTICE3:def 8; :: thesis: verum
end;
hence inf X << x ; :: thesis: verum