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