ex x, y being Element of Benzene st
( x [= y & not y = x "\/" ((x ` ) "/\" y) )

proof

set y = 2;
set x = 1;
reconsider x = 1, y = 2 as Element of Benzene by Th9, ENUMSET1:def 4;
for z being set st z in 1 holds
z in 2

proof

let z be set ; :: thesis: ( z in 1 implies z in 2 )
assume z in 1 ; :: thesis: z in 2
then z = 0 by CARD_1:87, TARSKI:def 1;
hence z in 2 by CARD_1:88, TARSKI:def 2; :: thesis: verum

end;

then 1 c= 2 by TARSKI:def 3;
then A15: x [= y by Th24;
x ` = 3 \ 1 by Th23;
then (x ` ) "/\" y = 0 by Th19;
then x "\/" ((x ` ) "/\" y) = x by Th29, LATTICES:39;
hence ex x, y being Element of Benzene st
( x [= y & not y = x "\/" ((x ` ) "/\" y) ) by A15; :: thesis: verum

end;

hence not Benzene is orthomodular by Def1; :: thesis: verum