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

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