ex x, y being Element of Benzene st

( x [= y & not y = x "\/" ((x `) "/\" y) )

( x [= y & not y = x "\/" ((x `) "/\" y) )

proof

hence
not Benzene is orthomodular
; :: thesis: verum
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

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;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

then
1 c= 2
;
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;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

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