let X be non empty set ; :: thesis: ( ( for x, y being set st x in X & y in X holds
x \/ y in X ) implies InclPoset X is with_suprema )
set L = InclPoset X;
assume A1: for x, y being set st x in X & y in X holds
x \/ y in X ; :: thesis: InclPoset X is with_suprema

now

let a, b be Element of (InclPoset X); :: thesis: ex_sup_of {a,b}, InclPoset X
ex c being Element of (InclPoset X) st
( {a,b} is_<=_than c & ( for d being Element of (InclPoset X) st {a,b} is_<=_than d holds
c <= d ) )

proof

take c = a "\/" b; :: thesis: ( {a,b} is_<=_than c & ( for d being Element of (InclPoset X) st {a,b} is_<=_than d holds
c <= d ) )
a \/ b = c by A1, Th8;
then ( a c= c & b c= c ) by XBOOLE_1:7;
then ( a <= c & b <= c ) by Th3;
hence {a,b} is_<=_than c by YELLOW_0:8; :: thesis: for d being Element of (InclPoset X) st {a,b} is_<=_than d holds
c <= d
let d be Element of (InclPoset X); :: thesis: ( {a,b} is_<=_than d implies c <= d )
assume A2: {a,b} is_<=_than d ; :: thesis: c <= d
a in {a,b} by TARSKI:def 2;
then A3: a <= d by A2, LATTICE3:def 9;
b in {a,b} by TARSKI:def 2;
then b <= d by A2, LATTICE3:def 9;
then ( a c= d & b c= d ) by A3, Th3;
then a \/ b c= d by XBOOLE_1:8;
then c c= d by A1, Th8;
hence c <= d by Th3; :: thesis: verum

end;

hence ex_sup_of {a,b}, InclPoset X by YELLOW_0:15; :: thesis: verum

end;

hence InclPoset X is with_suprema by YELLOW_0:20; :: thesis: verum