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 set ; :: 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 A2: ( q in A & q in B ) by XBOOLE_0:def 4;
reconsider A1 = A as non empty Subset of L by A1;
reconsider q1 = q as Element of A1 by A1, XBOOLE_0:def 4;
q1 = q1 "/\" q1 by YELLOW_0:25;
hence q in A "/\" B by A2; :: thesis: verum