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