let S, T be complete Scott TopLattice; :: thesis: ContMaps (S,T) is sups-inheriting SubRelStr of T |^ the carrier of S
set L = T |^ the carrier of S;
reconsider CS = ContMaps (S,T) as full SubRelStr of T |^ the carrier of S by Def3;
now :: thesis: for X being Subset of CS st ex_sup_of X,T |^ the carrier of S holds
"\/" (X,(T |^ the carrier of S)) in the carrier of CS
let X be Subset of CS; :: thesis: ( ex_sup_of X,T |^ the carrier of S implies "\/" (b1,(T |^ the carrier of S)) in the carrier of CS )
assume ex_sup_of X,T |^ the carrier of S ; :: thesis: "\/" (b1,(T |^ the carrier of S)) in the carrier of CS
per cases ( not X is empty or X is empty ) ;
suppose not X is empty ; :: thesis: "\/" (b1,(T |^ the carrier of S)) in the carrier of CS
hence "\/" (X,(T |^ the carrier of S)) in the carrier of CS by Th32; :: thesis: verum
end;
suppose X is empty ; :: thesis: "\/" (b1,(T |^ the carrier of S)) in the carrier of CS
then "\/" (X,(T |^ the carrier of S)) = Bottom (T |^ the carrier of S) by YELLOW_0:def 11;
then "\/" (X,(T |^ the carrier of S)) = S --> (Bottom T) by Th33;
hence "\/" (X,(T |^ the carrier of S)) in the carrier of CS by Def3; :: thesis: verum
end;
end;
end;
hence ContMaps (S,T) is sups-inheriting SubRelStr of T |^ the carrier of S by YELLOW_0:def 19; :: thesis: verum