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