let P, Q be non empty strict chain-complete flat Poset; :: thesis: for f being Function of P,Q st f . (Bottom P) = Bottom Q holds
f is continuous
let f be Function of P,Q; :: thesis: ( f . (Bottom P) = Bottom Q implies f is continuous )
assume A1: f . (Bottom P) = Bottom Q ; :: thesis: f is continuous
then reconsider f = f as monotone Function of P,Q by Thflat0501;
for K being non empty Chain of P holds f . (sup K) <= sup (f .: K)
proof
let K be non empty Chain of P; :: thesis: f . (sup K) <= sup (f .: K)
reconsider M = f .: K as non empty Chain of Q by POSET_1:1;
consider a being Element of P such that
B1: ( ( K = {a} & f .: K = {(f . a)} ) or ( K = {(Bottom P),a} & f .: K = {(f . (Bottom P)),(f . a)} ) ) by Thflat05;
per cases ( ( K = {a} & M = {(f . a)} ) or ( K = {(Bottom P),a} & M = {(Bottom Q),(f . a)} ) ) by A1, B1;
suppose ( K = {a} & M = {(f . a)} ) ; :: thesis: f . (sup K) <= sup (f .: K)
then ( sup K = a & sup M = f . a ) by YELLOW_0:39;
hence f . (sup K) <= sup (f .: K) ; :: thesis: verum
end;
suppose ( K = {(Bottom P),a} & M = {(Bottom Q),(f . a)} ) ; :: thesis: f . (sup K) <= sup (f .: K)
then ( sup K = a & sup M = f . a ) by Thflat0502;
hence f . (sup K) <= sup (f .: K) ; :: thesis: verum
end;
end;
end;
hence f is continuous by POSET_1:8; :: thesis: verum