let S, S9 be non empty RelStr ; for T, T9 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T9, the InternalRel of T9 #) holds
UPS (S,T) = UPS (S9,T9)
let T, T9 be non empty reflexive antisymmetric RelStr ; ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T9, the InternalRel of T9 #) implies UPS (S,T) = UPS (S9,T9) )
assume that
A1:
RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #)
and
A2:
RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T9, the InternalRel of T9 #)
; UPS (S,T) = UPS (S9,T9)
T |^ the carrier of S = T9 |^ the carrier of S9
by A1, A2, Th15;
then A3:
UPS (S9,T9) is full SubRelStr of T |^ the carrier of S
by Def4;
A4:
the carrier of (UPS (S,T)) = the carrier of (UPS (S9,T9))
proof
thus
the
carrier of
(UPS (S,T)) c= the
carrier of
(UPS (S9,T9))
XBOOLE_0:def 10 the carrier of (UPS (S9,T9)) c= the carrier of (UPS (S,T))
let x be
object ;
TARSKI:def 3 ( not x in the carrier of (UPS (S9,T9)) or x in the carrier of (UPS (S,T)) )
assume
x in the
carrier of
(UPS (S9,T9))
;
x in the carrier of (UPS (S,T))
then reconsider x1 =
x as
directed-sups-preserving Function of
S9,
T9 by Def4;
reconsider y =
x1 as
Function of
S,
T by A1, A2;
y is
directed-sups-preserving
hence
x in the
carrier of
(UPS (S,T))
by Def4;
verum
end;
UPS (S,T) is full SubRelStr of T |^ the carrier of S
by Def4;
hence
UPS (S,T) = UPS (S9,T9)
by A3, A4, YELLOW_0:57; verum