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

proof

assume a \ b = Bottom L ; :: thesis: a <= b
then (b "\/" a) "/\" (b "\/" ('not' b)) <= b "\/" (Bottom L) by Th17;
then (b "\/" a) "/\" (b "\/" ('not' b)) <= b by WAYBEL_1:3;
then (a "\/" b) "/\" (Top L) <= b by Th34;
then A1: a "\/" b <= b by WAYBEL_1:4;
a <= a "\/" b by YELLOW_0:22;
hence a <= b by A1, YELLOW_0:def 2; :: thesis: verum

end;

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

proof

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

end;