let T be non empty finite up-complete Poset; :: thesis: for S being Subset of holds S is inaccessible_by_directed_joins
let S be Subset of ; :: thesis: S is inaccessible_by_directed_joins
let D be non empty directed Subset of ; :: 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 D' = D as finite Subset of ;
D' c= D' ;
then reconsider E = D' as finite Subset of ;
consider x being Element of such that
A2: x in D and
A3: x is_>=_than E by WAYBEL_0:1;
A4: for b being Element of st D is_<=_than b holds
b >= x by A2, LATTICE3:def 9;
for c being Element of st D is_<=_than c & ( for b being Element of st D is_<=_than b holds
b >= c ) holds
c = x

proof

let c be Element of ; :: thesis: ( D is_<=_than c & ( for b being Element of 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 st D is_<=_than b holds
b >= c ; :: thesis: c = x
A7: x >= c by A3, A6;
c >= x by A2, A5, LATTICE3:def 9;
hence c = x by A7, ORDERS_2:25; :: 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