let P, Q be non empty strict chain-complete Poset; :: thesis: for z being Element of Q holds P --> z is continuous
let z be Element of Q; :: thesis: P --> z is continuous
set IT = P --> z;
for L being non empty Chain of P holds (P --> z) . (sup L) = sup ((P --> z) .: L)
proof
let L be non empty Chain of P; :: thesis: (P --> z) . (sup L) = sup ((P --> z) .: L)
set M = (P --> z) .: L;
for x being Element of Q st x in (P --> z) .: L holds
x <= z
proof
let x be Element of Q; :: thesis: ( x in (P --> z) .: L implies x <= z )
assume x in (P --> z) .: L ; :: thesis: x <= z
then consider a being object such that
A1: ( a in dom (P --> z) & a in L & x = (P --> z) . a ) by FUNCT_1:def 6;
thus x <= z by A1, FUNCOP_1:7; :: thesis: verum
end;
then A2: (P --> z) .: L is_<=_than z ;
for y being Element of Q st (P --> z) .: L is_<=_than y holds
z <= y
proof
let y be Element of Q; :: thesis: ( (P --> z) .: L is_<=_than y implies z <= y )
assume A3: (P --> z) .: L is_<=_than y ; :: thesis: z <= y
consider a being object such that
A4: a in L by XBOOLE_0:def 1;
a in the carrier of P by A4;
then A5: a in dom (P --> z) by FUNCOP_1:13;
(P --> z) . a = z by A4, FUNCOP_1:7;
then z in (P --> z) .: L by A4, A5, FUNCT_1:def 6;
hence z <= y by A3; :: thesis: verum
end;
then z = "\/" (((P --> z) .: L),Q) by A2, YELLOW_0:30;
hence (P --> z) . (sup L) = sup ((P --> z) .: L) by FUNCOP_1:7; :: thesis: verum
end;
hence P --> z is continuous by Th6; :: thesis: verum