let X be non empty set ; :: thesis: ( InclPoset X is lower-bounded implies meet X in X )
assume InclPoset X is lower-bounded ; :: thesis: meet X in X
then consider x being Element of (InclPoset X) such that
A1: x is_<=_than the carrier of (InclPoset X) by YELLOW_0:def 4;

now :: thesis: for y being object st y in x holds
y in meet X

let y be object ; :: thesis: ( y in x implies y in meet X )
assume A2: y in x ; :: thesis: y in meet X

now :: thesis: for Y being set st Y in X holds
y in Y

let Y be set ; :: thesis: ( Y in X implies y in Y )
assume Y in X ; :: thesis: y in Y
then reconsider Y9 = Y as Element of (InclPoset X) ;
x <= Y9 by A1;
then x c= Y9 by Th3;
hence y in Y by A2; :: thesis: verum

end;

hence y in meet X by SETFAM_1:def 1; :: thesis: verum

end;

then A3: x c= meet X ;
( x in X & meet X c= x ) by SETFAM_1:3;
hence meet X in X by A3, XBOOLE_0:def 10; :: thesis: verum