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
A5: A1 is full SubRelStr of T |^ the carrier of S and
A6: 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
A7: A2 is full SubRelStr of T |^ the carrier of S and
A8: 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 object ; :: 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 ex f being Function of S,T st
( x = f & f is continuous ) by A6;
hence x in the carrier of A2 by A8; :: thesis: verum
end;
let x be object ; :: 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 ex f being Function of S,T st
( x = f & f is continuous ) by A8;
hence x in the carrier of A1 by A6; :: thesis: verum
end;
hence A1 = A2 by A5, A7, YELLOW_0:57; :: thesis: verum