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 & a "|^|" b <= b ) by YELLOW_0:23;
then A2: ( a ` <= (a "|^|" b) ` & b ` <= (a "|^|" b) ` ) by Th7;
then A3: (a ` ) "|_|" (b ` ) <= ((a "|^|" b) ` ) "|_|" (b ` ) by WAYBEL_1:3;
(a "|^|" b) ` = (b ` ) "|_|" ((a "|^|" b) ` ) by A2, Th24;
hence (a ` ) "|_|" (b ` ) <= (a "|^|" b) ` by A3, LATTICE3:13; :: thesis: verum

end;

A4: 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 & b <= a "|_|" b ) by YELLOW_0:22;
then A5: ( (a "|_|" b) ` <= a ` & (a "|_|" b) ` <= b ` ) by Th7;
then ((a "|_|" b) ` ) "|^|" (b ` ) <= (a ` ) "|^|" (b ` ) by WAYBEL_1:2;
hence (a "|_|" b) ` <= (a ` ) "|^|" (b ` ) by A5, Th24; :: thesis: verum

end;

L is de_Morgan

proof

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;
A6: a "|^|" b = a |^| b by Th26;
A7: (a ` ) "|_|" (b ` ) = (a ` ) |_| (b ` ) by Th25;
( (a ` ) ` = a & (b ` ) ` = b ) by Th6;
then A8: ((a ` ) "|_|" (b ` )) ` <= a "|^|" b by A4;
((a "|^|" b) ` ) ` <= ((a ` ) "|_|" (b ` )) ` by A1, Th7;
then a "|^|" b <= ((a ` ) "|_|" (b ` )) ` by Th6;
hence ((a ` ) |_| (b ` )) ` = a |^| b by A6, A7, A8, ORDERS_2:25; :: thesis: verum

end;

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

end;

hence L is de_Morgan ; :: thesis: verum