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