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:69; :: thesis: verum