let T be non empty up-complete upper TopPoset; :: thesis: for A being Subset of T st A is open holds
A is upper
let A be Subset of T; :: thesis: ( A is open implies A is upper )
assume A1: A is open ; :: thesis: A is upper
A2: A in the topology of T by A1, PRE_TOPC:def 5;
reconsider BB = { ((downarrow x) ` ) where x is Element of T : verum } as prebasis of T by Def1;
consider F being Basis of T such that
A3: F c= FinMeetCl BB by CANTOR_1:def 5;
the topology of T c= UniCl F by CANTOR_1:def 2;
then consider Y being Subset-Family of T such that
A4: ( Y c= F & A = union Y ) by A2, CANTOR_1:def 1;
let x, y be Element of T; :: according to WAYBEL_0:def 20 :: thesis: ( not x in A or not x <= y or y in A )
assume x in A ; :: thesis: ( not x <= y or y in A )
then consider Z being set such that
A5: ( x in Z & Z in Y ) by A4, TARSKI:def 4;
Z in F by A4, A5;
then consider X being Subset-Family of T such that
A6: ( X c= BB & X is finite & Z = Intersect X ) by A3, CANTOR_1:def 4;
assume A7: x <= y ; :: thesis: y in A

now

let Q be set ; :: thesis: ( Q in X implies y in Q )
assume A8: Q in X ; :: thesis: y in Q
then Q in BB by A6;
then consider z being Element of T such that
A9: Q = (downarrow z) ` ;
( x in Q & downarrow z misses Q ) by A5, A6, A8, A9, SETFAM_1:58, XBOOLE_1:79;
then not x in downarrow z by XBOOLE_0:3;
then not x <= z by WAYBEL_0:17;
then not y <= z by A7, ORDERS_2:26;
then not y in downarrow z by WAYBEL_0:17;
hence y in Q by A9, XBOOLE_0:def 5; :: thesis: verum

end;

then y in Z by A6, SETFAM_1:58;
hence y in A by A4, A5, TARSKI:def 4; :: thesis: verum