let X be non empty set ; :: thesis: ( InclPoset X is with_infima implies for x, y being Element of (InclPoset X) holds x "/\" y c= x /\ y )
assume A1: InclPoset X is with_infima ; :: thesis: for x, y being Element of (InclPoset X) holds x "/\" y c= x /\ y
let x, y be Element of (InclPoset X); :: thesis: x "/\" y c= x /\ y
x "/\" y <= y by A1, YELLOW_0:23;
then A2: x "/\" y c= y by Th3;
x "/\" y <= x by A1, YELLOW_0:23;
then x "/\" y c= x by Th3;
hence x "/\" y c= x /\ y by A2, XBOOLE_1:19; :: thesis: verum