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