defpred S_{1}[ set ] means $1 is_a_fixpoint_of f;

set P = { x where x is Element of L : S_{1}[x] } ;

A2: { x where x is Element of L : S_{1}[x] } is Subset of L
from DOMAIN_1:sch 7();

consider a being Element of L such that

A3: a is_a_fixpoint_of f by A1, Th21;

A4: a in { x where x is Element of L : S_{1}[x] }
by A3;

reconsider P = { x where x is Element of L : S_{1}[x] } as Subset of L by A2;

A5: P is with_suprema

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

set P = { x where x is Element of L : S

A2: { x where x is Element of L : S

consider a being Element of L such that

A3: a is_a_fixpoint_of f by A1, Th21;

A4: a in { x where x is Element of L : S

reconsider P = { x where x is Element of L : S

A5: P is with_suprema

proof

P is with_infima
let x, y be Element of L; :: according to KNASTER:def 6 :: thesis: ( x in P & y in P implies ex z being Element of L st

( z in P & x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds

z [= z9 ) ) )

assume that

A6: x in P and

A7: y in P ; :: thesis: ex z being Element of L st

( z in P & x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds

z [= z9 ) )

consider a being Element of L such that

A8: x = a and

A9: a is_a_fixpoint_of f by A6;

consider b being Element of L such that

A10: y = b and

A11: b is_a_fixpoint_of f by A7;

reconsider a = a, b = b as Element of L ;

reconsider ab = a "\/" b as Element of L ;

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, Th32;

set z = (f,O) +. ab;

take (f,O) +. ab ; :: thesis: ( (f,O) +. ab in P & x [= (f,O) +. ab & y [= (f,O) +. ab & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds

(f,O) +. ab [= z9 ) )

thus (f,O) +. ab in P by A12; :: thesis: ( x [= (f,O) +. ab & y [= (f,O) +. ab & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds

(f,O) +. ab [= z9 ) )

thus ( x [= (f,O) +. ab & y [= (f,O) +. ab ) by A8, A10, A13; :: thesis: for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds

(f,O) +. ab [= z9

let z9 be Element of L; :: thesis: ( z9 in P & x [= z9 & y [= z9 implies (f,O) +. ab [= z9 )

assume that

A14: z9 in P and

A15: ( x [= z9 & y [= z9 ) ; :: thesis: (f,O) +. ab [= z9

A16: ex zz being Element of L st

( zz = z9 & zz is_a_fixpoint_of f ) by A14;

ab [= z9 by A8, A10, A15, FILTER_0:6;

hence (f,O) +. ab [= z9 by A1, A16, Th34; :: thesis: verum

end;( z in P & x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds

z [= z9 ) ) )

assume that

A6: x in P and

A7: y in P ; :: thesis: ex z being Element of L st

( z in P & x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds

z [= z9 ) )

consider a being Element of L such that

A8: x = a and

A9: a is_a_fixpoint_of f by A6;

consider b being Element of L such that

A10: y = b and

A11: b is_a_fixpoint_of f by A7;

reconsider a = a, b = b as Element of L ;

reconsider ab = a "\/" b as Element of L ;

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, Th32;

set z = (f,O) +. ab;

take (f,O) +. ab ; :: thesis: ( (f,O) +. ab in P & x [= (f,O) +. ab & y [= (f,O) +. ab & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds

(f,O) +. ab [= z9 ) )

thus (f,O) +. ab in P by A12; :: thesis: ( x [= (f,O) +. ab & y [= (f,O) +. ab & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds

(f,O) +. ab [= z9 ) )

thus ( x [= (f,O) +. ab & y [= (f,O) +. ab ) by A8, A10, A13; :: thesis: for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds

(f,O) +. ab [= z9

let z9 be Element of L; :: thesis: ( z9 in P & x [= z9 & y [= z9 implies (f,O) +. ab [= z9 )

assume that

A14: z9 in P and

A15: ( x [= z9 & y [= z9 ) ; :: thesis: (f,O) +. ab [= z9

A16: ex zz being Element of L st

( zz = z9 & zz is_a_fixpoint_of f ) by A14;

ab [= z9 by A8, A10, A15, FILTER_0:6;

hence (f,O) +. ab [= z9 by A1, A16, Th34; :: thesis: verum

proof

then reconsider P = P as non empty with_suprema with_infima Subset of L by A4, A5;
let x, y be Element of L; :: according to KNASTER:def 7 :: thesis: ( x in P & y in P implies ex z being Element of L st

( z in P & z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds

z9 [= z ) ) )

assume that

A17: x in P and

A18: y in P ; :: thesis: ex z being Element of L st

( z in P & z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds

z9 [= z ) )

consider a being Element of L such that

A19: x = a and

A20: a is_a_fixpoint_of f by A17;

consider b being Element of L such that

A21: y = b and

A22: b is_a_fixpoint_of f by A18;

reconsider a = a, b = b as Element of L ;

reconsider ab = a "/\" b as Element of L ;

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, Th33;

set z = (f,O) -. ab;

take (f,O) -. ab ; :: thesis: ( (f,O) -. ab in P & (f,O) -. ab [= x & (f,O) -. ab [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds

z9 [= (f,O) -. ab ) )

thus (f,O) -. ab in P by A23; :: thesis: ( (f,O) -. ab [= x & (f,O) -. ab [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds

z9 [= (f,O) -. ab ) )

thus ( (f,O) -. ab [= x & (f,O) -. ab [= y ) by A19, A21, A24; :: thesis: for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds

z9 [= (f,O) -. ab

let z9 be Element of L; :: thesis: ( z9 in P & z9 [= x & z9 [= y implies z9 [= (f,O) -. ab )

assume that

A25: z9 in P and

A26: ( z9 [= x & z9 [= y ) ; :: thesis: z9 [= (f,O) -. ab

A27: ex zz being Element of L st

( zz = z9 & zz is_a_fixpoint_of f ) by A25;

z9 [= ab by A19, A21, A26, FILTER_0:7;

hence z9 [= (f,O) -. ab by A1, A27, Th35; :: thesis: verum

end;( z in P & z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds

z9 [= z ) ) )

assume that

A17: x in P and

A18: y in P ; :: thesis: ex z being Element of L st

( z in P & z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds

z9 [= z ) )

consider a being Element of L such that

A19: x = a and

A20: a is_a_fixpoint_of f by A17;

consider b being Element of L such that

A21: y = b and

A22: b is_a_fixpoint_of f by A18;

reconsider a = a, b = b as Element of L ;

reconsider ab = a "/\" b as Element of L ;

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, Th33;

set z = (f,O) -. ab;

take (f,O) -. ab ; :: thesis: ( (f,O) -. ab in P & (f,O) -. ab [= x & (f,O) -. ab [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds

z9 [= (f,O) -. ab ) )

thus (f,O) -. ab in P by A23; :: thesis: ( (f,O) -. ab [= x & (f,O) -. ab [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds

z9 [= (f,O) -. ab ) )

thus ( (f,O) -. ab [= x & (f,O) -. ab [= y ) by A19, A21, A24; :: thesis: for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds

z9 [= (f,O) -. ab

let z9 be Element of L; :: thesis: ( z9 in P & z9 [= x & z9 [= y implies z9 [= (f,O) -. ab )

assume that

A25: z9 in P and

A26: ( z9 [= x & z9 [= y ) ; :: thesis: z9 [= (f,O) -. ab

A27: ex zz being Element of L st

( zz = z9 & zz is_a_fixpoint_of f ) by A25;

z9 [= ab by A19, A21, A26, FILTER_0:7;

hence z9 [= (f,O) -. ab by A1, A27, Th35; :: thesis: verum

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