let S, S' be non empty RelStr ; :: thesis: for T, T' being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of S',the InternalRel of S' #) & RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of T',the InternalRel of T' #) holds
UPS S,T = UPS S',T'
let T, T' be non empty reflexive antisymmetric RelStr ; :: thesis: ( RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of S',the InternalRel of S' #) & RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of T',the InternalRel of T' #) implies UPS S,T = UPS S',T' )
assume that
A1: RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of S',the InternalRel of S' #) and
A2: RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of T',the InternalRel of T' #) ; :: thesis: UPS S,T = UPS S',T'
T |^ the carrier of S = T' |^ the carrier of S' by A1, A2, Th15;
then A3: UPS S',T' is full SubRelStr of T |^ the carrier of S by Def4;
A4: the carrier of (UPS S,T) = the carrier of (UPS S',T')

proof

thus the carrier of (UPS S,T) c= the carrier of (UPS S',T') :: according to XBOOLE_0:def 10 :: thesis: the carrier of (UPS S',T') c= the carrier of (UPS S,T)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (UPS S,T) or x in the carrier of (UPS S',T') )
assume x in the carrier of (UPS S,T) ; :: thesis: x in the carrier of (UPS S',T')
then reconsider x1 = x as directed-sups-preserving Function of S,T by Def4;
reconsider y = x1 as Function of S',T' by A1, A2;
y is directed-sups-preserving

proof

let X be Subset of ; :: according to WAYBEL_0:def 37 :: thesis: ( X is empty or not X is directed or y preserves_sup_of X )
reconsider Y = X as Subset of by A1;
assume ( not X is empty & X is directed ) ; :: thesis: y preserves_sup_of X
then ( not Y is empty & Y is directed ) by A1, WAYBEL_0:3;
then x1 preserves_sup_of Y by WAYBEL_0:def 37;
hence y preserves_sup_of X by A1, A2, WAYBEL_0:65; :: thesis: verum

end;

hence x in the carrier of (UPS S',T') by Def4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (UPS S',T') or x in the carrier of (UPS S,T) )
assume x in the carrier of (UPS S',T') ; :: thesis: x in the carrier of (UPS S,T)
then reconsider x1 = x as directed-sups-preserving Function of S',T' by Def4;
reconsider y = x1 as Function of S,T by A1, A2;
y is directed-sups-preserving

proof

let X be Subset of ; :: according to WAYBEL_0:def 37 :: thesis: ( X is empty or not X is directed or y preserves_sup_of X )
reconsider Y = X as Subset of by A1;
assume ( not X is empty & X is directed ) ; :: thesis: y preserves_sup_of X
then ( not Y is empty & Y is directed ) by A1, WAYBEL_0:3;
then x1 preserves_sup_of Y by WAYBEL_0:def 37;
hence y preserves_sup_of X by A1, A2, WAYBEL_0:65; :: thesis: verum

end;

hence x in the carrier of (UPS S,T) by Def4; :: thesis: verum

end;

UPS S,T is full SubRelStr of T |^ the carrier of S by Def4;
hence UPS S,T = UPS S',T' by A3, A4, YELLOW_0:58; :: thesis: verum