thus ( T is Scott implies for S being Subset of T holds
( S is open iff S is upper ) ) by Def4; :: thesis: ( ( for S being Subset of T holds
( S is open iff S is upper ) ) implies T is Scott )
assume A1: for S being Subset of T holds
( S is open iff S is upper ) ; :: thesis: T is Scott
let S be Subset of T; :: according to WAYBEL11:def 4 :: thesis: ( S is open iff ( S is inaccessible_by_directed_joins & S is upper ) )
thus ( S is open iff ( S is inaccessible_by_directed_joins & S is upper ) ) by A1; :: thesis: verum