let L be Nelson_Algebra; :: thesis: for a, b being Element of L holds (a => b) "/\" ((- a) "\/" b) = (- a) "\/" b
let a, b be Element of L; :: thesis: (a => b) "/\" ((- a) "\/" b) = (- a) "\/" b
A1: - ((- a) "\/" b) < - ((a => b) "/\" ((- a) "\/" b))
proof
A2: - ((- a) "\/" b) = (- (- a)) "/\" (- b) by Th1;
A3: (- (- a)) "/\" (- b) = a "/\" (- b) by ROBBINS3:def 6;
a "/\" (- b) < - (a => b) by Def9;
then (- ((- a) "\/" b)) "\/" (- ((- a) "\/" b)) < (- (a => b)) "\/" (- ((- a) "\/" b)) by A2, A3, Lm1;
hence - ((- a) "\/" b) < - ((a => b) "/\" ((- a) "\/" b)) by Th8; :: thesis: verum
end;
A4: (- a) "\/" b <= (a => b) "/\" ((- a) "\/" b)
proof
(- a) "\/" b <= a => b by Th11;
hence (- a) "\/" b <= (a => b) "/\" ((- a) "\/" b) ; :: thesis: verum
end;
(a => b) "/\" ((- a) "\/" b) <= (- a) "\/" b by Th6, A1, Th5;
hence (a => b) "/\" ((- a) "\/" b) = (- a) "\/" b by A4, Th3; :: thesis: verum