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 Th9, ENUMSET1:def 4;
suppose A1: a = 0 ; :: thesis: (a `) ` = a
then a ` = 3 by Th23;
hence (a `) ` = a by A1, Th23; :: thesis: verum
end;
suppose A2: a = 1 ; :: thesis: (a `) ` = a
then a ` = 3 \ 1 by Th23;
hence (a `) ` = a by A2, Th23; :: thesis: verum
end;
suppose A3: a = 3 \ 1 ; :: thesis: (a `) ` = a
then a ` = 1 by Th23;
hence (a `) ` = a by A3, Th23; :: thesis: verum
end;
suppose A4: a = 2 ; :: thesis: (a `) ` = a
then a ` = 3 \ 2 by Th23;
hence (a `) ` = a by A4, Th23; :: thesis: verum
end;
suppose A5: a = 3 \ 2 ; :: thesis: (a `) ` = a
then a ` = 2 by Th23;
hence (a `) ` = a by A5, Th23; :: thesis: verum
end;
suppose A6: a = 3 ; :: thesis: (a `) ` = a
then a ` = 0 by Th23;
hence (a `) ` = a by A6, Th23; :: thesis: verum
end;
end;
end;
hence A7: Benzene is involutive ; :: thesis: ( Benzene is with_Top & Benzene is de_Morgan )
A8: 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 Th9, ENUMSET1:def 4;
suppose A9: a = 0 ; :: thesis: a "\/" (a `) = 3
then a ` = 3 by Th23;
hence a "\/" (a `) = 3 by A9, Th26; :: thesis: verum
end;
suppose A10: a = 1 ; :: thesis: a "\/" (a `) = 3
then a ` = 3 \ 1 by Th23;
hence a "\/" (a `) = 3 by A10, Th21; :: thesis: verum
end;
suppose A11: a = 3 \ 1 ; :: thesis: a "\/" (a `) = 3
then a ` = 1 by Th23;
hence a "\/" (a `) = 3 by A11, Th21; :: thesis: verum
end;
suppose A12: a = 2 ; :: thesis: a "\/" (a `) = 3
then a ` = 3 \ 2 by Th23;
hence a "\/" (a `) = 3 by A12, Th22; :: thesis: verum
end;
suppose A13: a = 3 \ 2 ; :: thesis: a "\/" (a `) = 3
then a ` = 2 by Th23;
hence a "\/" (a `) = 3 by A13, Th22; :: thesis: verum
end;
suppose a = 3 ; :: thesis: a "\/" (a `) = 3
hence a "\/" (a `) = 3 by Th27; :: 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 A8;
hence a "\/" (a `) = b "\/" (b `) by A8; :: thesis: verum
end;
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 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;
hence Benzene is de_Morgan by A7, Th4; :: thesis: verum