let T be reflexive transitive antisymmetric with_suprema RelStr ; :: thesis: for D being non empty finite directed Subset of T holds sup D in D
let D be non empty finite directed Subset of T; :: thesis: sup D in D
D c= D ;
then reconsider E = D as finite Subset of D ;
consider x being Element of T such that
A1: x in D and
A2: x is_>=_than E by WAYBEL_0:1;
A3: for b being Element of T st D is_<=_than b holds
b >= x by A1;
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
A4: D is_<=_than c and
A5: for b being Element of T st D is_<=_than b holds
b >= c ; :: thesis: c = x
A6: x >= c by A2, A5;
c >= x by A1, A4;
hence c = x by A6, ORDERS_2:2; :: thesis: verum
end;
then ex_sup_of D,T by A2, A3;
hence sup D in D by A1, A2, A3, YELLOW_0:def 9; :: thesis: verum