let L be reflexive antisymmetric with_infima RelStr ; :: thesis: for A, B being Subset of L holds A /\ B c= A "/\" B
let A, B be Subset of L; :: thesis: A /\ B c= A "/\" B
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in A /\ B or q in A "/\" B )
assume A1: q in A /\ B ; :: thesis: q in A "/\" B
then reconsider A1 = A as non empty Subset of L ;
reconsider q1 = q as Element of A1 by A1, XBOOLE_0:def 4;
A2: q1 = q1 "/\" q1 by YELLOW_0:25;
q in B by A1, XBOOLE_0:def 4;
hence q in A "/\" B by A2; :: thesis: verum