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

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 ) )
a /\ b = c by A1, Th9;
then ( c c= a & c c= b ) by XBOOLE_1:17;
then ( c <= a & c <= b ) 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: d <= a by A2, LATTICE3:def 8;
b in {a,b} by TARSKI:def 2;
then d <= b by A2, LATTICE3:def 8;
then ( d c= a & d c= b ) by A3, Th3;
then d c= a /\ b by 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