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:3;
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:2;
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:25; :: thesis: verum

end;

hence L is de_Morgan by ROBBINS1:def 23; :: thesis: verum