defpred S1[ set ] means $1 is_a_fixpoint_of f;
set P = { x where x is Element of L : S1[x] } ;
consider a being Element of L such that
A2:
a is_a_fixpoint_of f
by A1, Th24;
A3:
a in { x where x is Element of L : S1[x] }
by A2;
{ x where x is Element of L : S1[x] } is Subset of L
from DOMAIN_1:sch 7();
then reconsider P = { x where x is Element of L : S1[x] } as Subset of L ;
A4:
P is with_suprema
proof
let x,
y be
Element of
L;
:: according to KNASTER:def 8 :: thesis: ( x in P & y in P implies ex z being Element of L st
( z in P & x [= z & y [= z & ( for z' being Element of L st z' in P & x [= z' & y [= z' holds
z [= z' ) ) )
assume A5:
(
x in P &
y in P )
;
:: thesis: ex z being Element of L st
( z in P & x [= z & y [= z & ( for z' being Element of L st z' in P & x [= z' & y [= z' holds
z [= z' ) )
then consider a being
Element of
L such that A6:
(
x = a &
a is_a_fixpoint_of f )
;
consider b being
Element of
L such that A7:
(
y = b &
b is_a_fixpoint_of f )
by A5;
reconsider a =
a,
b =
b as
Element of
L ;
reconsider ab =
a "\/" b as
Element of
L ;
consider O being
Ordinal such that A8:
(
card O c= card the
carrier of
L &
f,
O +. ab is_a_fixpoint_of f &
a [= f,
O +. ab &
b [= f,
O +. ab )
by A1, A6, A7, Th35;
set z =
f,
O +. ab;
take
f,
O +. ab
;
:: thesis: ( f,O +. ab in P & x [= f,O +. ab & y [= f,O +. ab & ( for z' being Element of L st z' in P & x [= z' & y [= z' holds
f,O +. ab [= z' ) )
thus
f,
O +. ab in P
by A8;
:: thesis: ( x [= f,O +. ab & y [= f,O +. ab & ( for z' being Element of L st z' in P & x [= z' & y [= z' holds
f,O +. ab [= z' ) )
thus
(
x [= f,
O +. ab &
y [= f,
O +. ab )
by A6, A7, A8;
:: thesis: for z' being Element of L st z' in P & x [= z' & y [= z' holds
f,O +. ab [= z'
let z' be
Element of
L;
:: thesis: ( z' in P & x [= z' & y [= z' implies f,O +. ab [= z' )
assume A9:
(
z' in P &
x [= z' &
y [= z' )
;
:: thesis: f,O +. ab [= z'
then consider zz being
Element of
L such that A10:
(
zz = z' &
zz is_a_fixpoint_of f )
;
A11:
(
a = f . a &
b = f . b )
by A6, A7, ABIAN:def 3;
(
a [= ab &
b [= ab )
by LATTICES:22;
then
(
f . a [= f . ab &
f . b [= f . ab )
by A1, QUANTAL1:def 12;
then A12:
ab [= f . ab
by A11, FILTER_0:6;
ab [= z'
by A6, A7, A9, FILTER_0:6;
hence
f,
O +. ab [= z'
by A1, A10, A12, Th37;
:: thesis: verum
end;
P is with_infima
proof
let x,
y be
Element of
L;
:: according to KNASTER:def 9 :: thesis: ( x in P & y in P implies ex z being Element of L st
( z in P & z [= x & z [= y & ( for z' being Element of L st z' in P & z' [= x & z' [= y holds
z' [= z ) ) )
assume A13:
(
x in P &
y in P )
;
:: thesis: ex z being Element of L st
( z in P & z [= x & z [= y & ( for z' being Element of L st z' in P & z' [= x & z' [= y holds
z' [= z ) )
then consider a being
Element of
L such that A14:
(
x = a &
a is_a_fixpoint_of f )
;
consider b being
Element of
L such that A15:
(
y = b &
b is_a_fixpoint_of f )
by A13;
reconsider a =
a,
b =
b as
Element of
L ;
reconsider ab =
a "/\" b as
Element of
L ;
consider O being
Ordinal such that A16:
(
card O c= card the
carrier of
L &
f,
O -. ab is_a_fixpoint_of f &
f,
O -. ab [= a &
f,
O -. ab [= b )
by A1, A14, A15, Th36;
set z =
f,
O -. ab;
take
f,
O -. ab
;
:: thesis: ( f,O -. ab in P & f,O -. ab [= x & f,O -. ab [= y & ( for z' being Element of L st z' in P & z' [= x & z' [= y holds
z' [= f,O -. ab ) )
thus
f,
O -. ab in P
by A16;
:: thesis: ( f,O -. ab [= x & f,O -. ab [= y & ( for z' being Element of L st z' in P & z' [= x & z' [= y holds
z' [= f,O -. ab ) )
thus
(
f,
O -. ab [= x &
f,
O -. ab [= y )
by A14, A15, A16;
:: thesis: for z' being Element of L st z' in P & z' [= x & z' [= y holds
z' [= f,O -. ab
let z' be
Element of
L;
:: thesis: ( z' in P & z' [= x & z' [= y implies z' [= f,O -. ab )
assume A17:
(
z' in P &
z' [= x &
z' [= y )
;
:: thesis: z' [= f,O -. ab
then consider zz being
Element of
L such that A18:
(
zz = z' &
zz is_a_fixpoint_of f )
;
A19:
(
a = f . a &
b = f . b )
by A14, A15, ABIAN:def 3;
(
ab [= a &
ab [= b )
by LATTICES:23;
then
(
f . ab [= f . a &
f . ab [= f . b )
by A1, QUANTAL1:def 12;
then A20:
f . ab [= ab
by A19, FILTER_0:7;
z' [= ab
by A14, A15, A17, FILTER_0:7;
hence
z' [= f,
O -. ab
by A1, A18, A20, Th38;
:: thesis: verum
end;
then reconsider P = P as non empty with_suprema with_infima Subset of L by A3, A4;
take
latt P
; :: thesis: ex P being non empty with_suprema with_infima Subset of L st
( P = { x where x is Element of L : x is_a_fixpoint_of f } & latt P = latt P )
take
P
; :: thesis: ( P = { x where x is Element of L : x is_a_fixpoint_of f } & latt P = latt P )
thus
P = { x where x is Element of L : x is_a_fixpoint_of f }
; :: thesis: latt P = latt P
thus
latt P = latt P
; :: thesis: verum