let A1, A2 be strict RelStr ; :: thesis: ( A1 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of A1 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) & A2 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of A2 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) implies A1 = A2 )
assume that
A4: ( A1 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of A1 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) ) and
A5: ( A2 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of A2 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) ) ; :: thesis: A1 = A2
the carrier of A1 = the carrier of A2

proof

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

let x be set ; :: thesis: ( x in the carrier of A1 implies x in the carrier of A2 )
assume x in the carrier of A1 ; :: thesis: x in the carrier of A2
then consider f being Function of S,T such that
A6: ( x = f & f is continuous ) by A4;
thus x in the carrier of A2 by A5, A6; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of A2 or x in the carrier of A1 )
assume x in the carrier of A2 ; :: thesis: x in the carrier of A1
then consider f being Function of S,T such that
A7: ( x = f & f is continuous ) by A5;
thus x in the carrier of A1 by A4, A7; :: thesis: verum

end;

hence A1 = A2 by A4, A5, YELLOW_0:58; :: thesis: verum