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;
A2: x in X ;
A3: meet X c= x by SETFAM_1:4;

now

let y be set ; :: thesis: ( y in x implies y in meet X )
assume A4: y in x ; :: thesis: y in meet X

now

let Y be set ; :: thesis: ( Y in X implies y in Y )
assume Y in X ; :: thesis: y in Y
then reconsider Y' = Y as Element of (InclPoset X) ;
x <= Y' by A1, LATTICE3:def 8;
then x c= Y by Th3;
hence y in Y by A4; :: thesis: verum

end;

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

end;

then x c= meet X by TARSKI:def 3;
hence meet X in X by A2, A3, XBOOLE_0:def 10; :: thesis: verum