let U1, U2 be strict RelStr ; :: thesis: ( U1 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of U1 iff x is directed-sups-preserving Function of S,T ) ) & U2 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of U2 iff x is directed-sups-preserving Function of S,T ) ) implies U1 = U2 )
assume that
A3: U1 is full SubRelStr of T |^ the carrier of S and
A4: for x being set holds
( x in the carrier of U1 iff x is directed-sups-preserving Function of S,T ) and
A5: U2 is full SubRelStr of T |^ the carrier of S and
A6: for x being set holds
( x in the carrier of U2 iff x is directed-sups-preserving Function of S,T ) ; :: thesis: U1 = U2
the carrier of U1 = the carrier of U2

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: the carrier of U2 c= the carrier of U1

let x be object ; :: thesis: ( x in the carrier of U1 implies x in the carrier of U2 )
assume x in the carrier of U1 ; :: thesis: x in the carrier of U2
then x is directed-sups-preserving Function of S,T by A4;
hence x in the carrier of U2 by A6; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of U2 or x in the carrier of U1 )
assume x in the carrier of U2 ; :: thesis: x in the carrier of U1
then x is directed-sups-preserving Function of S,T by A6;
hence x in the carrier of U1 by A4; :: thesis: verum

end;

hence U1 = U2 by A3, A5, YELLOW_0:57; :: thesis: verum