let L be transitive antisymmetric with_infima lower-bounded RelStr ; :: thesis: for a, b, c being Element of L st a misses c & b <= c holds
a misses b
let a, b, c be Element of L; :: thesis: ( a misses c & b <= c implies a misses b )
assume that
A1: a misses c and
A2: b <= c ; :: thesis: a misses b
a "/\" c = Bottom L by A1;
then A3: a "/\" b <= Bottom L by A2, Th6;
Bottom L <= a "/\" b by YELLOW_0:44;
then a "/\" b = Bottom L by A3, YELLOW_0:def 3;
hence a misses b ; :: thesis: verum