let S, T be complete LATTICE; :: thesis: for A being Subset of (UPS (S,T)) holds sup A = "\/" (A,(T |^ the carrier of S))
let A be Subset of (UPS (S,T)); :: thesis: sup A = "\/" (A,(T |^ the carrier of S))
A1: UPS (S,T) is full sups-inheriting SubRelStr of T |^ the carrier of S by Def4, Th26;
ex_sup_of A,T |^ the carrier of S by YELLOW_0:17;
then "\/" (A,(T |^ the carrier of S)) in the carrier of (UPS (S,T)) by A1, YELLOW_0:def 19;
hence sup A = "\/" (A,(T |^ the carrier of S)) by A1, YELLOW_0:68; :: thesis: verum