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