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_infima )
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_infima

now :: thesis: for a, b being Element of (InclPoset X) holds ex_inf_of {a,b}, InclPoset X

let a, b be Element of (InclPoset X); :: thesis: ex_inf_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, Th9;
then c c= b by XBOOLE_1:17;
then A3: c <= b by Th3;
c c= a by A2, XBOOLE_1:17;
then c <= a 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 d <= b by A4;
then A5: d c= b by Th3;
a in {a,b} by TARSKI:def 2;
then d <= a by A4;
then d c= a by Th3;
then d c= a /\ b by A5, XBOOLE_1:19;
then d c= c by A1, Th9;
hence c >= d by Th3; :: thesis: verum

end;

hence ex_inf_of {a,b}, InclPoset X by YELLOW_0:16; :: thesis: verum

end;

hence InclPoset X is with_infima by YELLOW_0:21; :: thesis: verum