let L be non empty antisymmetric with_infima lower-bounded RelStr ; :: thesis: for x, y being Element of L st x is atom & y is atom & x <> y holds
x "/\" y = Bottom L
let x, y be Element of L; :: thesis: ( x is atom & y is atom & x <> y implies x "/\" y = Bottom L )
assume that
A1: x is atom and
A2: y is atom and
A3: x <> y and
A4: x "/\" y <> Bottom L ; :: thesis: contradiction
Bottom L <= x "/\" y by YELLOW_0:44;
then A5: Bottom L < x "/\" y by A4, ORDERS_2:def 6;
A6: x "/\" y <= y by YELLOW_0:23;
x "/\" y <= x by YELLOW_0:23;
then x = x "/\" y by A1, A5
.= y by A2, A5, A6 ;
hence contradiction by A3; :: thesis: verum