let L be non empty Lattice-like with_suprema with_infima PartialOrdered OrderInvolutive naturally_sup-generated naturally_inf-generated OrthoLattRelStr ; :: thesis: L is de_Morgan
A1: for x, y being Element of L holds (x `) "|_|" (y `) <= (x "|^|" y) `
proof
let a, b be Element of L; :: thesis: (a `) "|_|" (b `) <= (a "|^|" b) `
set i = a "|^|" b;
set s = (a `) "|_|" (b `);
a "|^|" b <= a by YELLOW_0:23;
then a ` <= (a "|^|" b) ` by Th7;
then A2: (a `) "|_|" (b `) <= ((a "|^|" b) `) "|_|" (b `) by WAYBEL_1:2;
a "|^|" b <= b by YELLOW_0:23;
then b ` <= (a "|^|" b) ` by Th7;
then (a "|^|" b) ` = (b `) "|_|" ((a "|^|" b) `) by Th24;
hence (a `) "|_|" (b `) <= (a "|^|" b) ` by A2, LATTICE3:13; :: thesis: verum
end;
A3: for x, y being Element of L holds (x "|_|" y) ` <= (x `) "|^|" (y `)
proof
let a, b be Element of L; :: thesis: (a "|_|" b) ` <= (a `) "|^|" (b `)
set i = (a `) "|^|" (b `);
set s = a "|_|" b;
a <= a "|_|" b by YELLOW_0:22;
then (a "|_|" b) ` <= a ` by Th7;
then A4: ((a "|_|" b) `) "|^|" (b `) <= (a `) "|^|" (b `) by WAYBEL_1:1;
b <= a "|_|" b by YELLOW_0:22;
then (a "|_|" b) ` <= b ` by Th7;
hence (a "|_|" b) ` <= (a `) "|^|" (b `) by A4, Th24; :: thesis: verum
end;
for x, y being Element of L holds ((x `) |_| (y `)) ` = x |^| y
proof
let a, b be Element of L; :: thesis: ((a `) |_| (b `)) ` = a |^| b
set s = (a `) "|_|" (b `);
set i = a "|^|" b;
( (a `) ` = a & (b `) ` = b ) by Th6;
then A5: ((a `) "|_|" (b `)) ` <= a "|^|" b by A3;
((a "|^|" b) `) ` <= ((a `) "|_|" (b `)) ` by A1, Th7;
then A6: a "|^|" b <= ((a `) "|_|" (b `)) ` by Th6;
( a "|^|" b = a |^| b & (a `) "|_|" (b `) = (a `) |_| (b `) ) by Th25, Th26;
hence ((a `) |_| (b `)) ` = a |^| b by A5, A6, ORDERS_2:2; :: thesis: verum
end;
hence L is de_Morgan by ROBBINS1:def 23; :: thesis: verum