set B = Benzene ;
for a being Element of Benzene holds (a ` ) ` = a

proof

let a be Element of Benzene ; :: thesis: (a ` ) ` = a

per cases ( a = 0 or a = 1 or a = 3 \ 1 or a = 2 or a = 3 \ 2 or a = 3 ) by LemBen, ENUMSET1:def 4;

suppose x: a = 0 ; :: thesis: (a ` ) ` = a

then a ` = 3 by twU;
hence (a ` ) ` = a by x, twU; :: thesis: verum

end;

suppose x: a = 1 ; :: thesis: (a ` ) ` = a

then a ` = 3 \ 1 by twU;
hence (a ` ) ` = a by x, twU; :: thesis: verum

end;

suppose x: a = 3 \ 1 ; :: thesis: (a ` ) ` = a

then a ` = 1 by twU;
hence (a ` ) ` = a by x, twU; :: thesis: verum

end;

suppose x: a = 2 ; :: thesis: (a ` ) ` = a

then a ` = 3 \ 2 by twU;
hence (a ` ) ` = a by x, twU; :: thesis: verum

end;

suppose x: a = 3 \ 2 ; :: thesis: (a ` ) ` = a

then a ` = 2 by twU;
hence (a ` ) ` = a by x, twU; :: thesis: verum

end;

suppose x: a = 3 ; :: thesis: (a ` ) ` = a

then a ` = 0 by twU;
hence (a ` ) ` = a by x, twU; :: thesis: verum

end;

end;

end;

hence I: Benzene is involutive by ROBBINS3:def 6; :: thesis: ( Benzene is with_Top & Benzene is de_Morgan )
B: for a being Element of Benzene holds a "\/" (a ` ) = 3

proof

let a be Element of Benzene ; :: thesis: a "\/" (a ` ) = 3

per cases ( a = 0 or a = 1 or a = 3 \ 1 or a = 2 or a = 3 \ 2 or a = 3 ) by LemBen, ENUMSET1:def 4;

suppose x: a = 0 ; :: thesis: a "\/" (a ` ) = 3

then a ` = 3 by twU;
hence a "\/" (a ` ) = 3 by x, Bot2; :: thesis: verum

end;

suppose x: a = 1 ; :: thesis: a "\/" (a ` ) = 3

then a ` = 3 \ 1 by twU;
hence a "\/" (a ` ) = 3 by x, Haczyk3; :: thesis: verum

end;

suppose x: a = 3 \ 1 ; :: thesis: a "\/" (a ` ) = 3

then a ` = 1 by twU;
hence a "\/" (a ` ) = 3 by x, Haczyk3; :: thesis: verum

end;

suppose x: a = 2 ; :: thesis: a "\/" (a ` ) = 3

then a ` = 3 \ 2 by twU;
hence a "\/" (a ` ) = 3 by x, Haczyk4; :: thesis: verum

end;

suppose x: a = 3 \ 2 ; :: thesis: a "\/" (a ` ) = 3

then a ` = 2 by twU;
hence a "\/" (a ` ) = 3 by x, Haczyk4; :: thesis: verum

end;

suppose a = 3 ; :: thesis: a "\/" (a ` ) = 3

hence a "\/" (a ` ) = 3 by Bot1; :: thesis: verum

end;

end;

end;

thus Benzene is with_Top :: thesis: Benzene is de_Morgan

proof

let a, b be Element of Benzene ; :: according to ROBBINS3:def 7 :: thesis: a "\/" (a ` ) = b "\/" (b ` )
a "\/" (a ` ) = 3 by B;
hence a "\/" (a ` ) = b "\/" (b ` ) by B; :: thesis: verum

end;

thus Benzene is de_Morgan :: thesis: verum

proof

for a, b being Element of Benzene st a [= b holds
b ` [= a `

proof

let a, b be Element of Benzene ; :: thesis: ( a [= b implies b ` [= a ` )
reconsider x = a, y = b as Subset of {0 ,1,2} by CosikX;
reconsider x = x, y = y as Subset of 3 by CARD_1:89;
A1: a ` = x ` by BenDef;
A2: b ` = y ` by BenDef;
assume a [= b ; :: thesis: b ` [= a `
then x c= y by Inkl;
then y ` c= x ` by SUBSET_1:31;
hence b ` [= a ` by A1, A2, Inkl; :: thesis: verum

end;

hence Benzene is de_Morgan by theo, I; :: thesis: verum

end;