let T be non empty reflexive transitive antisymmetric up-complete Scott TopRelStr ; :: 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 S is upper ; :: 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: ( not "\/" (D,T) in S or ex b₁ being Element of the carrier of T st
( b₁ in D & ( for b₂ being Element of the carrier of T holds
( not b₂ in D or not b₁ <= b₂ or b₂ in S ) ) ) )
assume sup D in S ; :: thesis: ex b₁ being Element of the carrier of T st
( b₁ in D & ( for b₂ being Element of the carrier of T holds
( not b₂ in D or not b₁ <= b₂ or b₂ in S ) ) )
then S meets D by A1, WAYBEL11:def 1;
then consider y being object such that
A2: y in S and
A3: y in D by XBOOLE_0:3;
reconsider y = y as Element of T by A2;
take y ; :: thesis: ( y in D & ( for b₁ being Element of the carrier of T holds
( not b₁ in D or not y <= b₁ or b₁ in S ) ) )
thus ( y in D & ( for b₁ being Element of the carrier of T holds
( not b₁ in D or not y <= b₁ or b₁ in S ) ) ) by A1, A2, A3, WAYBEL_0:def 20; :: thesis: verum

end;

end;

assume that
A4: S is upper and
A5: 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: ( not "\/" (D,T) in S or not D misses S )
assume sup D in S ; :: thesis: not D misses S
then consider y being Element of T such that
A6: y in D and
A7: for x being Element of T st x in D & x >= y holds
x in S by A5;
y >= y by YELLOW_0:def 1;
then y in S by A6, A7;
hence not D misses S by A6, XBOOLE_0:3; :: thesis: verum

end;

hence S is open by A4; :: thesis: verum