let K be reflexive antisymmetric with_suprema with_infima RelStr ; :: thesis: for k1, k2 being Element of K holds k1 "/\" (k1 "\/" k2) = k1
let k1, k2 be Element of K; :: thesis: k1 "/\" (k1 "\/" k2) = k1
( k1 <= k1 & k1 <= k1 "\/" k2 & ( for k3 being Element of K st k3 <= k1 & k3 <= k1 "\/" k2 holds
k3 <= k1 ) ) by Lm1;
hence k1 "/\" (k1 "\/" k2) = k1 by Def14; :: thesis: verum