let L be reflexive antisymmetric with_infima RelStr ; :: thesis: for A, B being lower Subset of L holds A "/\" B = A /\ B
let A, B be lower Subset of L; :: thesis: A "/\" B = A /\ B
thus A "/\" B c= A /\ B :: according to XBOOLE_0:def 10 :: thesis: A /\ B c= A "/\" B
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in A "/\" B or q in A /\ B )
assume q in A "/\" B ; :: thesis: q in A /\ B
then consider x, y being Element of L such that
A1: q = x "/\" y and
A2: x in A and
A3: y in B ;
A4: ex z being Element of L st
( x >= z & y >= z & ( for c being Element of L st x >= c & y >= c holds
z >= c ) ) by LATTICE3:def 11;
then x "/\" y <= y by LATTICE3:def 14;
then A5: q in B by A1, A3, WAYBEL_0:def 19;
x "/\" y <= x by A4, LATTICE3:def 14;
then q in A by A1, A2, WAYBEL_0:def 19;
hence q in A /\ B by A5, XBOOLE_0:def 4; :: thesis: verum
end;
thus A /\ B c= A "/\" B by Th49; :: thesis: verum