let L be AD_Lattice; :: thesis: for x being Element of L holds x "\/" x = x
let x be Element of L; :: thesis: x "\/" x = x
A8: for x, y being Element of L holds (x "\/" x) "/\" y = x "/\" (y "\/" y)
proof
let x, y be Element of L; :: thesis: (x "\/" x) "/\" y = x "/\" (y "\/" y)
set z = x;
(x "/\" y) "\/" (x "/\" y) = x "/\" (y "\/" y) by LATTICES:def 11;
hence (x "\/" x) "/\" y = x "/\" (y "\/" y) by DefD; :: thesis: verum
end;
A27: x "/\" (x "\/" x) = x
proof
(x "\/" x) "/\" x = x "/\" (x "\/" x) by A8;
hence x "/\" (x "\/" x) = x by DefA1; :: thesis: verum
end;
A43: for x, y being Element of L holds (x "\/" y) "/\" (y "\/" y) = y "\/" y
proof
let x, y be Element of L; :: thesis: (x "\/" y) "/\" (y "\/" y) = y "\/" y
(x "\/" y) "/\" (y "\/" y) = ((x "\/" y) "/\" y) "\/" ((x "\/" y) "/\" y) by LATTICES:def 11
.= y "\/" ((x "\/" y) "/\" y) by DefA1
.= y "\/" y by DefA1 ;
hence (x "\/" y) "/\" (y "\/" y) = y "\/" y ; :: thesis: verum
end;
A49: (x "\/" x) "\/" (x "\/" x) = x "\/" x
proof
(x "\/" x) "/\" (x "\/" x) = ((x "\/" x) "/\" x) "\/" ((x "\/" x) "/\" x) by LATTICES:def 11
.= x "\/" ((x "\/" x) "/\" x) by DefA1
.= x "\/" x by DefA1 ;
hence (x "\/" x) "\/" (x "\/" x) = x "\/" x by ROBBINS3:def 3; :: thesis: verum
end;
set R = x "\/" x;
x "\/" x = (x "\/" x) "/\" (x "\/" x) by A43
.= x by A27, A49, A8 ;
hence x "\/" x = x ; :: thesis: verum