set B = Benzene ;

for a being Element of Benzene holds (a `) ` = a

A8: for a being Element of Benzene holds a "\/" (a `) = 3

b ` [= a `

for a being Element of Benzene holds (a `) ` = a

proof

hence A7:
Benzene is involutive
; :: thesis: ( Benzene is with_Top & Benzene is de_Morgan )
let a be Element of Benzene; :: thesis: (a `) ` = a

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

end;

A8: for a being Element of Benzene holds a "\/" (a `) = 3

proof

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

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

end;

proof

for a, b being Element of Benzene st a [= b holds
let a, b be Element of Benzene; :: according to ROBBINS3:def 7 :: thesis: a "\/" (a `) = b "\/" (b `)

a "\/" (a `) = 3 by A8;

hence a "\/" (a `) = b "\/" (b `) by A8; :: thesis: verum

end;a "\/" (a `) = 3 by A8;

hence a "\/" (a `) = b "\/" (b `) by A8; :: thesis: verum

b ` [= a `

proof

hence
Benzene is de_Morgan
by A7, Th4; :: thesis: verum
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 Th11;

reconsider x = x, y = y as Subset of 3 by CARD_1:51;

assume a [= b ; :: thesis: b ` [= a `

then x c= y by Th24;

then A14: y ` c= x ` by SUBSET_1:12;

( a ` = x ` & b ` = y ` ) by Def4;

hence b ` [= a ` by A14, Th24; :: thesis: verum

end;reconsider x = a, y = b as Subset of {0,1,2} by Th11;

reconsider x = x, y = y as Subset of 3 by CARD_1:51;

assume a [= b ; :: thesis: b ` [= a `

then x c= y by Th24;

then A14: y ` c= x ` by SUBSET_1:12;

( a ` = x ` & b ` = y ` ) by Def4;

hence b ` [= a ` by A14, Th24; :: thesis: verum