let L be D_Lattice; :: thesis: for b, a being Element of L st not b [= a holds
ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F )
let b, a be Element of L; :: thesis: ( not b [= a implies ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F ) )
assume A1:
not b [= a
; :: thesis: ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F )
set A = (SF_have b) \ (SF_have a);
A2:
(SF_have b) \ (SF_have a) <> {}
by A1, Th21;
for Z being set st Z <> {} & Z c= (SF_have b) \ (SF_have a) & Z is c=-linear holds
ex Y being set st
( Y in (SF_have b) \ (SF_have a) & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
by Th20;
then consider Y being set such that
A3:
( Y in (SF_have b) \ (SF_have a) & ( for Z being set st Z in (SF_have b) \ (SF_have a) & Z <> Y holds
not Y c= Z ) )
by A2, LATTICE4:3;
reconsider Y = Y as Filter of L by A3, Th19;
A4:
( not a in Y & b in Y )
by A3, Th19;
A5:
Y <> the carrier of L
by A3, Th19;
Y is prime
proof
let a1,
a2 be
Element of
L;
:: according to FILTER_0:def 6 :: thesis: ( ( not a1 "\/" a2 in Y or a1 in Y or a2 in Y ) & ( ( not a1 in Y & not a2 in Y ) or a1 "\/" a2 in Y ) )
thus
( not
a1 "\/" a2 in Y or
a1 in Y or
a2 in Y )
:: thesis: ( ( not a1 in Y & not a2 in Y ) or a1 "\/" a2 in Y )proof
assume A6:
(
a1 "\/" a2 in Y & not
a1 in Y & not
a2 in Y )
;
:: thesis: contradiction
set F1 =
<.(<.a1.) \/ Y).);
set F2 =
<.(<.a2.) \/ Y).);
A7:
( not
a in <.(<.a1.) \/ Y).) or not
a in <.(<.a2.) \/ Y).) )
proof
assume A8:
(
a in <.(<.a1.) \/ Y).) &
a in <.(<.a2.) \/ Y).) )
;
:: thesis: contradiction
then consider c1 being
Element of
L such that A9:
(
c1 in Y &
a1 "/\" c1 [= a )
by LATTICE4:6;
consider c2 being
Element of
L such that A10:
(
c2 in Y &
a2 "/\" c2 [= a )
by A8, LATTICE4:6;
set c =
c1 "/\" c2;
A11:
c1 "/\" c2 in Y
by A9, A10, FILTER_0:def 1;
(
a1 "/\" (c1 "/\" c2) [= a1 "/\" c1 &
a2 "/\" (c1 "/\" c2) [= a2 "/\" c2 )
by LATTICES:23, LATTICES:27;
then
(
a1 "/\" (c1 "/\" c2) [= a &
a2 "/\" (c1 "/\" c2) [= a )
by A9, A10, LATTICES:25;
then
(a1 "/\" (c1 "/\" c2)) "\/" (a2 "/\" (c1 "/\" c2)) [= a
by FILTER_0:6;
then A12:
(a1 "\/" a2) "/\" (c1 "/\" c2) [= a
by LATTICES:def 11;
(a1 "\/" a2) "/\" (c1 "/\" c2) in Y
by A6, A11, FILTER_0:def 1;
hence
contradiction
by A4, A12, FILTER_0:9;
:: thesis: verum
end;
A13:
(
a1 in <.a1.) &
a2 in <.a2.) )
;
(
<.a1.) c= <.(<.a1.) \/ Y).) &
<.a2.) c= <.(<.a2.) \/ Y).) )
by LATTICE4:5;
then A14:
(
a1 in <.(<.a1.) \/ Y).) &
a2 in <.(<.a2.) \/ Y).) )
by A13;
A15:
(
Y c= <.(<.a1.) \/ Y).) &
Y c= <.(<.a2.) \/ Y).) )
by LATTICE4:5;
then
(
<.(<.a1.) \/ Y).) in (SF_have b) \ (SF_have a) or
<.(<.a2.) \/ Y).) in (SF_have b) \ (SF_have a) )
by A4, A7, Lm1;
hence
contradiction
by A3, A6, A14, A15;
:: thesis: verum
end;
thus
( ( not
a1 in Y & not
a2 in Y ) or
a1 "\/" a2 in Y )
by FILTER_0:10;
:: thesis: verum
end;
then
Y in F_primeSet L
by A5;
hence
ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F )
by A4; :: thesis: verum