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