let L be transitive antisymmetric with_infima lower-bounded RelStr ; :: thesis: for a, b, c being Element of L st a misses b holds
a "/\" c misses b "/\" c
let a, b, c be Element of L; :: thesis: ( a misses b implies a "/\" c misses b "/\" c )
assume A1: a misses b ; :: thesis: a "/\" c misses b "/\" c
(a "/\" c) "/\" (b "/\" c) = c "/\" (a "/\" (b "/\" c)) by LATTICE3:16
.= (c "/\" (a "/\" b)) "/\" c by LATTICE3:16
.= (c "/\" (Bottom L)) "/\" c by A1
.= (Bottom L) "/\" c by Th25
.= Bottom L by Th25 ;
hence a "/\" c misses b "/\" c ; :: thesis: verum