let X be non empty set ; :: thesis: for x, y being Element of (InclPoset X) st x /\ y in X holds
x "/\" y = x /\ y
let x, y be Element of (InclPoset X); :: thesis: ( x /\ y in X implies x "/\" y = x /\ y )
assume x /\ y in X ; :: thesis: x "/\" y = x /\ y
then reconsider z = x /\ y as Element of (InclPoset X) ;
z c= y by XBOOLE_1:17;
then A1: z <= y by Th3;

A2: now :: thesis: for c being Element of (InclPoset X) st c <= x & c <= y holds
c <= z

let c be Element of (InclPoset X); :: thesis: ( c <= x & c <= y implies c <= z )
assume ( c <= x & c <= y ) ; :: thesis: c <= z
then ( c c= x & c c= y ) by Th3;
then c c= z by XBOOLE_1:19;
hence c <= z by Th3; :: thesis: verum

end;

z c= x by XBOOLE_1:17;
then z <= x by Th3;
hence x "/\" y = x /\ y by A1, A2, LATTICE3:def 14; :: thesis: verum