let L be Lattice; :: thesis:
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:
A2: for H being Filter of L st r in H holds
H = the carrier of L

let H be Filter of L; :: thesis:
assume A3: r in H ; :: thesis:
thus H c= the carrier of L ; :: according to XBOOLE_0:def 10 :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in the carrier of L ; :: thesis:
then reconsider p = x as Element of L ;
r "/\" p = r by A1;
then r [= p by LATTICES:4;
hence x in H by A3, Th9; :: thesis:

end;

let F be Filter of L; :: thesis:
assume A4: F <> the carrier of L ; :: thesis:
set X = { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } ;
A5: 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 )

let x be set ; :: thesis:
assume x in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } ; :: thesis:
then ex A being Subset of L st
( x = A & F c= A & A is Filter of L & A <> the carrier of L ) ;
hence ( x is Subset of L & x is Filter of L ) ; :: thesis:

end;

A6: 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 )

let X1 be set ; :: thesis:
assume X1 in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } ; :: thesis:
then ex A being Subset of L st
( X1 = A & F c= A & A is Filter of L & A <> the carrier of L ) ;
hence ( F,X1 are_c=-comparable & X1 <> the carrier of L ) ; :: thesis:

end;

A7: 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 ) )

set x = the Element of F;
let Z be set ; :: thesis:
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:
take Y = union (Z \/ {F}); :: thesis:
F in {F} by TARSKI:def 1;
then A10: F in Z \/ {F} by XBOOLE_0:def 3;
the Element of F in F ;
then reconsider V = Y as non empty set by A10, TARSKI:def 4;
V c= the carrier of L

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in V ; :: thesis:
then consider X1 being set such that
A11: x in X1 and
A12: X1 in Z \/ {F} by TARSKI:def 4;
( X1 in Z or X1 in {F} ) by A12, XBOOLE_0:def 3;
then X1 is Subset of L by A5, A8;
hence x in the carrier of L by A11; :: thesis:

end;

then reconsider V = V as non empty Subset of L ;

let p, q be Element of L; :: thesis:
thus ( p in V & q in V implies p "/\" q in V ) :: thesis:

assume p in V ; :: thesis:
then consider X1 being set such that
A13: p in X1 and
A14: X1 in Z \/ {F} by TARSKI:def 4;
A15: ( X1 in Z or X1 in {F} ) by A14, XBOOLE_0:def 3;
then A16: ( ( 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 ) by A8, TARSKI:def 1;
assume q in V ; :: thesis:
then consider X2 being set such that
A17: q in X2 and
A18: X2 in Z \/ {F} by TARSKI:def 4;
A19: ( X2 in Z or X2 in {F} ) by A18, XBOOLE_0:def 3;
then ( ( 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 by A6, A9, A16, ORDINAL1:def 8;
then A20: ( X1 c= X2 or X2 c= X1 ) ;
A21: X1 is Filter of L by A5, A8, A15, TARSKI:def 1;
X2 is Filter of L by A5, A8, A19, TARSKI:def 1;
then ( p "/\" q in X1 or p "/\" q in X2 ) by A13, A17, A20, A21, Th9;
hence p "/\" q in V by A14, A18, TARSKI:def 4; :: thesis:

end;

end;

then reconsider V = V as Filter of L by Th8;

assume r in V ; :: thesis:
then consider X1 being set such that
A24: r in X1 and
A25: X1 in Z \/ {F} by TARSKI:def 4;
( X1 in Z or X1 in {F} ) by A25, 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 ) } or X1 = F ) by A8, TARSKI:def 1;
then ex A being Subset of L st
( X1 = A & F c= A & A is Filter of L & A <> the carrier of L ) by A4;
hence contradiction by A2, A24; :: thesis:

end;

then A26: V <> the carrier of L ;
F c= V by A10, TARSKI:def 4;
hence Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } by A26; :: thesis:
let X1 be set ; :: thesis:
assume X1 in Z ; :: thesis:
then X1 in Z \/ {F} by XBOOLE_0:def 3;
hence X1 c= Y by ZFMISC_1:74; :: thesis:

end;

F in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } by A4;
then consider Y being set such that
A27: Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } and
A28: 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 A7, ORDERS_1:65;
consider H being Subset of L such that
A29: Y = H and
A30: F c= H and
A31: H is Filter of L and
A32: H <> the carrier of L by A27;
reconsider H = H as Filter of L by A31;
take H ; :: thesis:
thus ( F c= H & H <> the carrier of L ) by A30, A32; :: according to FILTER_0:def 3 :: thesis:
let G be Filter of L; :: thesis:
assume that
A33: H c= G and
A34: G <> the carrier of L ; :: thesis:
F c= G by A30, A33;
then G in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } by A34;
hence H = G by A28, A29, A33; :: thesis: