%------------------------------------------------------------------------------
% Identity Function is Continuous
%
% All references are to BA Davey and HA Priestly "Introduction to Lattices and
% Orders", CUP, 1990
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            25/12/07  Initial Version
%------------------------------------------------------------------------------

scott_identity_continuity[T:TYPE,(IMPORTING orders@directed_orders[T])
                          le:(directed_complete_partial_order?)]: THEORY

BEGIN

  IMPORTING scott_continuity[T,T,le,le],
            topology@identity_continuity[T,scott_open_sets[T,le]]

  id_scott_continuous: JUDGEMENT I[T] HAS_TYPE scott_continuous

END scott_identity_continuity