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 :: thesis: for a, b being Element of (InclPoset X) holds ex_sup_of {a,b}, InclPoset X

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 ) )
A2: a \/ b = c by A1, Th8;
then b c= c by XBOOLE_1:7;
then A3: b <= c by Th3;
a c= c by A2, XBOOLE_1:7;
then a <= c by Th3;
hence {a,b} is_<=_than c by A3, 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 A4: {a,b} is_<=_than d ; :: thesis: c <= d
b in {a,b} by TARSKI:def 2;
then b <= d by A4;
then A5: b c= d by Th3;
a in {a,b} by TARSKI:def 2;
then a <= d by A4;
then a c= d by Th3;
then a \/ b c= d by A5, 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