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

proof

set x = 1;
set y = 2;
reconsider x = 1, y = 2 as Element of Benzene by LemBen, ENUMSET1:def 4;
d: x ` = 3 \ 1 by twU;
f: 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;

1 c= 2 by f, TARSKI:def 3;
then a: x [= y by Inkl;
x "\/" ((x ` ) "/\" y) = x

proof

(x ` ) "/\" y = 0 by Haczyk1, d;
hence x "\/" ((x ` ) "/\" y) = x by Stan0, LATTICES:39; :: thesis: verum

end;

hence ex x, y being Element of Benzene st
( x [= y & not y = x "\/" ((x ` ) "/\" y) ) by a; :: thesis: verum

end;

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