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 "\/" (b₁,(T |^ the carrier of S)) in the carrier of CS )
assume ex_sup_of X,T |^ the carrier of S ; :: thesis: "\/" (b₁,(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: "\/" (b₁,(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: "\/" (b₁,(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