let L be D_Lattice; for a, b 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 a, b be Element of L; ( not b [= a implies 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);
assume
not b [= a
; ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F )
then A1:
(SF_have b) \ (SF_have a) <> {}
by Th19;
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 Th18;
then consider Y being set such that
A2:
Y in (SF_have b) \ (SF_have a)
and
A3:
for Z being set st Z in (SF_have b) \ (SF_have a) & Z <> Y holds
not Y c= Z
by A1, LATTICE4:1;
reconsider Y = Y as Filter of L by A2, Th17;
A4:
b in Y
by A2, Th17;
A5:
not a in Y
by A2, Th17;
A6:
Y is prime
proof
let a1,
a2 be
Element of
L;
FILTER_0:def 5 ( ( 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 )
( ( not a1 in Y & not a2 in Y ) or a1 "\/" a2 in Y )proof
set F2 =
<.(<.a2.) \/ Y).);
set F1 =
<.(<.a1.) \/ Y).);
assume that A7:
a1 "\/" a2 in Y
and A8:
not
a1 in Y
and A9:
not
a2 in Y
;
contradiction
A10:
<.a1.) c= <.(<.a1.) \/ Y).)
by LATTICE4:2;
a1 in <.a1.)
;
then A11:
a1 in <.(<.a1.) \/ Y).)
by A10;
A12:
Y c= <.(<.a1.) \/ Y).)
by LATTICE4:2;
A13:
<.a2.) c= <.(<.a2.) \/ Y).)
by LATTICE4:2;
a2 in <.a2.)
;
then A14:
a2 in <.(<.a2.) \/ Y).)
by A13;
A15:
Y c= <.(<.a2.) \/ Y).)
by LATTICE4:2;
( not
a in <.(<.a1.) \/ Y).) or not
a in <.(<.a2.) \/ Y).) )
proof
assume that A16:
a in <.(<.a1.) \/ Y).)
and A17:
a in <.(<.a2.) \/ Y).)
;
contradiction
consider c1 being
Element of
L such that A18:
c1 in Y
and A19:
a1 "/\" c1 [= a
by A16, LATTICE4:3;
consider c2 being
Element of
L such that A20:
c2 in Y
and A21:
a2 "/\" c2 [= a
by A17, LATTICE4:3;
set c =
c1 "/\" c2;
a2 "/\" (c1 "/\" c2) [= a2 "/\" c2
by LATTICES:6, LATTICES:9;
then A22:
a2 "/\" (c1 "/\" c2) [= a
by A21, LATTICES:7;
a1 "/\" (c1 "/\" c2) [= a1 "/\" c1
by LATTICES:6, LATTICES:9;
then
a1 "/\" (c1 "/\" c2) [= a
by A19, LATTICES:7;
then
(a1 "/\" (c1 "/\" c2)) "\/" (a2 "/\" (c1 "/\" c2)) [= a
by A22, FILTER_0:6;
then A23:
(a1 "\/" a2) "/\" (c1 "/\" c2) [= a
by LATTICES:def 11;
c1 "/\" c2 in Y
by A18, A20, FILTER_0:8;
then
(a1 "\/" a2) "/\" (c1 "/\" c2) in Y
by A7, FILTER_0:8;
hence
contradiction
by A5, A23, FILTER_0:9;
verum
end;
then
(
<.(<.a1.) \/ Y).) in (SF_have b) \ (SF_have a) or
<.(<.a2.) \/ Y).) in (SF_have b) \ (SF_have a) )
by A4, A12, A15, Lm1;
hence
contradiction
by A3, A8, A9, A11, A14, A12, A15;
verum
end;
thus
( ( not
a1 in Y & not
a2 in Y ) or
a1 "\/" a2 in Y )
by FILTER_0:10;
verum
end;
Y <> the carrier of L
by A2, Th17;
then
Y in F_primeSet L
by A6;
hence
ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F )
by A5, A4; verum