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
A1: k1 <= k1 ;
A2: k1 <= k1 "\/" k2 by Lm1;
for k3 being Element of K st k3 <= k1 & k3 <= k1 "\/" k2 holds
k3 <= k1 ;
hence k1 "/\" (k1 "\/" k2) = k1 by A1, A2, Def14; :: thesis: verum