let L be non empty Boolean RelStr ; :: thesis: for a, b being Element of L holds
( a "/\" b = Bottom L iff a \ b = a )
let a, b be Element of L; :: thesis: ( a "/\" b = Bottom L iff a \ b = a )
thus ( a "/\" b = Bottom L implies a \ b = a ) :: thesis: ( a \ b = a implies a "/\" b = Bottom L )

proof

assume a "/\" b = Bottom L ; :: thesis: a \ b = a
then a <= 'not' b by WAYBEL_1:82;
then a "/\" a <= a "/\" ('not' b) by Th6;
then A1: a <= a "/\" ('not' b) by Th2;
a \ b <= a by YELLOW_0:23;
hence a \ b = a by A1, YELLOW_0:def 3; :: thesis: verum

end;

thus ( a \ b = a implies a "/\" b = Bottom L ) :: thesis: verum

proof

assume a \ b = a ; :: thesis: a "/\" b = Bottom L
then ('not' a) "\/" ('not' ('not' b)) = 'not' a by Th36;
then a "/\" (('not' a) "\/" b) <= a "/\" ('not' a) by WAYBEL_1:87;
then (a "/\" ('not' a)) "\/" (a "/\" b) <= a "/\" ('not' a) by WAYBEL_1:def 3;
then (Bottom L) "\/" (a "/\" b) <= a "/\" ('not' a) by Th34;
then (Bottom L) "\/" (a "/\" b) <= Bottom L by Th34;
then A2: a "/\" b <= Bottom L by WAYBEL_1:3;
Bottom L <= a "/\" b by YELLOW_0:44;
hence a "/\" b = Bottom L by A2, YELLOW_0:def 3; :: thesis: verum

end;