let L be reflexive antisymmetric with_infima RelStr ; :: thesis: for a, b being Element of L holds
( a = a "/\" b iff a <= b )
let a, b be Element of L; :: thesis: ( a = a "/\" b iff a <= b )
( a <= a & ( for d being Element of L st d <= a & d <= b holds
a >= d ) ) ;
hence ( a = a "/\" b iff a <= b ) by Th23; :: thesis: verum