let L be reflexive antisymmetric with_suprema with_infima RelStr ; :: thesis: for a, b being Element of L holds

( a "/\" b = b iff a "\/" b = a )

let a, b be Element of L; :: thesis: ( a "/\" b = b iff a "\/" b = a )

thus ( a "/\" b = b implies a "\/" b = a ) :: thesis: ( a "\/" b = a implies a "/\" b = b )

then b <= a by YELLOW_0:22;

hence a "/\" b = b by YELLOW_0:25; :: thesis: verum

( a "/\" b = b iff a "\/" b = a )

let a, b be Element of L; :: thesis: ( a "/\" b = b iff a "\/" b = a )

thus ( a "/\" b = b implies a "\/" b = a ) :: thesis: ( a "\/" b = a implies a "/\" b = b )

proof

assume
a "\/" b = a
; :: thesis: a "/\" b = b
assume
a "/\" b = b
; :: thesis: a "\/" b = a

then b <= a by YELLOW_0:23;

hence a "\/" b = a by YELLOW_0:24; :: thesis: verum

end;then b <= a by YELLOW_0:23;

hence a "\/" b = a by YELLOW_0:24; :: thesis: verum

then b <= a by YELLOW_0:22;

hence a "/\" b = b by YELLOW_0:25; :: thesis: verum