let L be Lattice; :: thesis: ( L is lower-bounded implies for F being Filter of L st F <> the carrier of L holds
ex H being Filter of L st
( F c= H & H is being_ultrafilter ) )
given r being Element of L such that A1:
for p being Element of L holds
( r "/\" p = r & p "/\" r = r )
; :: according to LATTICES:def 13 :: thesis: for F being Filter of L st F <> the carrier of L holds
ex H being Filter of L st
( F c= H & H is being_ultrafilter )
let F be Filter of L; :: thesis: ( F <> the carrier of L implies ex H being Filter of L st
( F c= H & H is being_ultrafilter ) )
assume A2:
F <> the carrier of L
; :: thesis: ex H being Filter of L st
( F c= H & H is being_ultrafilter )
set X = { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } ;
A3:
F in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) }
by A2;
A4:
for x being set st x in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } holds
( x is Subset of L & x is Filter of L )
A5:
for X1 being set st X1 in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } holds
( F,X1 are_c=-comparable & X1 <> the carrier of L )
A6:
for H being Filter of L st r in H holds
H = the carrier of L
for Z being set st Z c= { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & Z is c=-linear holds
ex Y being set st
( Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
proof
let Z be
set ;
:: thesis: ( Z c= { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & Z is c=-linear implies ex Y being set st
( Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) )
assume that A8:
Z c= { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) }
and A9:
Z is
c=-linear
;
:: thesis: ex Y being set st
( Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
take Y =
union (Z \/ {F});
:: thesis: ( Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
consider x being
Element of
F;
A10:
x in F
;
F in {F}
by TARSKI:def 1;
then A11:
F in Z \/ {F}
by XBOOLE_0:def 3;
then reconsider V =
Y as non
empty set by A10, TARSKI:def 4;
V c= the
carrier of
L
then reconsider V =
V as non
empty Subset of
L ;
V is
Filter of
L
proof
let p be
Element of
L;
:: according to FILTER_0:def 1 :: thesis: for q being Element of L holds
( ( p in V & q in V ) iff p "/\" q in V )let q be
Element of
L;
:: thesis: ( ( p in V & q in V ) iff p "/\" q in V )
thus
(
p in V &
q in V implies
p "/\" q in V )
:: thesis: ( p "/\" q in V implies ( p in V & q in V ) )proof
assume
p in V
;
:: thesis: ( not q in V or p "/\" q in V )
then consider X1 being
set such that A13:
(
p in X1 &
X1 in Z \/ {F} )
by TARSKI:def 4;
assume
q in V
;
:: thesis: p "/\" q in V
then consider X2 being
set such that A14:
(
q in X2 &
X2 in Z \/ {F} )
by TARSKI:def 4;
( (
X1 in Z or
X1 in {F} ) & (
X2 in Z or
X2 in {F} ) )
by A13, A14, XBOOLE_0:def 3;
then
( ( (
X1 in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } &
X1 in Z ) or
X1 = F ) & ( (
X2 in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } &
X2 in Z ) or
X2 = F ) )
by A8, TARSKI:def 1;
then
(
X1,
X2 are_c=-comparable &
X1 <> the
carrier of
L &
X2 <> the
carrier of
L &
X1 is
Filter of
L &
X2 is
Filter of
L )
by A2, A4, A5, A9, ORDINAL1:def 9;
then
( (
X1 c= X2 or
X2 c= X1 ) &
X1 <> the
carrier of
L &
X2 <> the
carrier of
L &
X1 is
Filter of
L &
X2 is
Filter of
L )
by XBOOLE_0:def 9;
then
(
p "/\" q in X1 or
p "/\" q in X2 )
by A13, A14, Th9;
hence
p "/\" q in V
by A13, A14, TARSKI:def 4;
:: thesis: verum
end;
assume
p "/\" q in V
;
:: thesis: ( p in V & q in V )
then consider X1 being
set such that A15:
(
p "/\" q in X1 &
X1 in Z \/ {F} )
by TARSKI:def 4;
(
X1 in Z or
X1 in {F} )
by A15, XBOOLE_0:def 3;
then
X1 is
Filter of
L
by A4, A8, TARSKI:def 1;
then
(
p in X1 &
q in X1 )
by A15, Def1;
hence
(
p in V &
q in V )
by A15, TARSKI:def 4;
:: thesis: verum
end;
then reconsider V =
V as
Filter of
L ;
A16:
F c= V
then
(
V <> the
carrier of
L &
V is
Subset of
L )
;
hence
Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) }
by A16;
:: thesis: for X1 being set st X1 in Z holds
X1 c= Y
let X1 be
set ;
:: thesis: ( X1 in Z implies X1 c= Y )
assume
X1 in Z
;
:: thesis: X1 c= Y
then
X1 in Z \/ {F}
by XBOOLE_0:def 3;
hence
X1 c= Y
by ZFMISC_1:92;
:: thesis: verum
end;
then consider Y being set such that
A18:
( Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & ( for Z being set st Z in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & Z <> Y holds
not Y c= Z ) )
by A3, ORDERS_1:175;
consider H being Subset of L such that
A19:
( Y = H & F c= H & H is Filter of L & H <> the carrier of L )
by A18;
reconsider H = H as Filter of L by A19;
take
H
; :: thesis: ( F c= H & H is being_ultrafilter )
thus
( F c= H & H <> the carrier of L )
by A19; :: according to FILTER_0:def 4 :: thesis: for H being Filter of L st H c= H & H <> the carrier of L holds
H = H
let G be Filter of L; :: thesis: ( H c= G & G <> the carrier of L implies H = G )
assume A20:
( H c= G & G <> the carrier of L )
; :: thesis: H = G
then
( G is Subset of L & F c= G )
by A19, XBOOLE_1:1;
then
G in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) }
by A20;
hence
H = G
by A18, A19, A20; :: thesis: verum