let T be non empty finite up-complete Poset; :: thesis: for S being Subset of T holds S is inaccessible
let S be Subset of T; :: thesis: S is inaccessible
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 A1: sup D in S ; :: thesis: not D misses S
sup D in D

proof

reconsider D9 = D as finite Subset of T ;
D9 c= D9 ;
then reconsider E = D9 as finite Subset of D ;
consider x being Element of T such that
A2: x in D and
A3: x is_>=_than E by WAYBEL_0:1;
A4: for b being Element of T st D is_<=_than b holds
b >= x by A2;
for c being Element of T st D is_<=_than c & ( for b being Element of T st D is_<=_than b holds
b >= c ) holds
c = x

proof

let c be Element of T; :: thesis: ( D is_<=_than c & ( for b being Element of T st D is_<=_than b holds
b >= c ) implies c = x )
assume that
A5: D is_<=_than c and
A6: for b being Element of T st D is_<=_than b holds
b >= c ; :: thesis: c = x
A7: x >= c by A3, A6;
c >= x by A2, A5;
hence c = x by A7, ORDERS_2:2; :: thesis: verum

end;

then ex_sup_of D,T by A3, A4, YELLOW_0:def 7;
hence sup D in D by A2, A3, A4, YELLOW_0:def 9; :: thesis: verum

end;

hence not D misses S by A1, XBOOLE_0:3; :: thesis: verum