let L be reflexive antisymmetric with_infima RelStr ; :: thesis: for a being Element of L holds a "/\" a = a

let a be Element of L; :: thesis: a "/\" a = a

a <= a ;

then ( a "/\" a <= a & a <= a "/\" a ) by YELLOW_0:23;

hence a "/\" a = a by YELLOW_0:def 3; :: thesis: verum

let a be Element of L; :: thesis: a "/\" a = a

a <= a ;

then ( a "/\" a <= a & a <= a "/\" a ) by YELLOW_0:23;

hence a "/\" a = a by YELLOW_0:def 3; :: thesis: verum