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 object st z in 1 holds
z in 2
proof
let z be object ; :: thesis: ( z in 1 implies z in 2 )
assume z in 1 ; :: thesis: z in 2
then z = 0 by CARD_1:49, TARSKI:def 1;
hence z in 2 by CARD_1:50, TARSKI:def 2; :: thesis: verum
end;
then 1 c= 2 ;
then A15: x [= y by Th24;
x ` = 3 \ 1 by Th23;
then (x `) "/\" y = 0 by Th19;
then x "\/" ((x `) "/\" y) = x by Th29;
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 ; :: thesis: verum