let T be Scott TopLattice; :: thesis: for S being Subset of T holds
( S is open iff ( S is upper & S is property(S) ) )
let S be Subset of T; :: thesis: ( S is open iff ( S is upper & S is property(S) ) )

hereby :: thesis: ( S is upper & S is property(S) implies S is open )

assume A1: S is open ; :: thesis: ( S is upper & S is property(S) )
hence A2: S is upper by Def4; :: thesis: S is property(S)
thus S is property(S) :: thesis: verum

proof

let D be non empty directed Subset of T; :: according to WAYBEL11:def 3 :: thesis: ( sup D in S implies ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) ) )
assume A3: sup D in S ; :: thesis: ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) )
S is inaccessible by A1, Def4;
then S meets D by A3;
then consider y being object such that
A4: y in S and
A5: y in D by XBOOLE_0:3;
reconsider y = y as Element of T by A4;
take y ; :: thesis: ( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) )
thus ( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) ) by A2, A4, A5; :: thesis: verum

end;

end;

assume that
A6: S is upper and
A7: S is property(S) ; :: thesis: S is open
S is inaccessible

proof

let D be non empty directed Subset of T; :: according to WAYBEL11:def 1 :: thesis: ( sup D in S implies D meets S )
assume sup D in S ; :: thesis: D meets S
then consider y being Element of T such that
A8: y in D and
A9: for x being Element of T st x in D & x >= y holds
x in S by A7;
y >= y by YELLOW_0:def 1;
then y in S by A8, A9;
hence D meets S by A8, XBOOLE_0:3; :: thesis: verum

end;

hence S is open by A6, Def4; :: thesis: verum