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 )

proof

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;

assume a "\/" b = a ; :: thesis: a "/\" b = b
then b <= a by YELLOW_0:22;
hence a "/\" b = b by YELLOW_0:25; :: thesis: verum