let S, S9 be non empty RelStr ; :: thesis: 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 ; :: thesis: ( 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 #) ; :: thesis: 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)) :: according to XBOOLE_0:def 10 :: thesis: the carrier of (UPS (S9,T9)) c= the carrier of (UPS (S,T))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (UPS (S,T)) or x in the carrier of (UPS (S9,T9)) )
assume x in the carrier of (UPS (S,T)) ; :: thesis: x in the carrier of (UPS (S9,T9))
then reconsider x1 = x as directed-sups-preserving Function of S,T by Def4;
reconsider y = x1 as Function of S9,T9 by A1, A2;
y is directed-sups-preserving
proof
let X be Subset of S9; :: 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 S 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 (S9,T9)) by Def4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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)) ; :: thesis: 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
proof
let X be Subset of S; :: 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 S9 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 (S9,T9) by A3, A4, YELLOW_0:57; :: thesis: verum