let A1, A2 be strict full SubRelStr of T |^ the carrier of S; :: thesis: ( ( for f being Function of S,T holds
( f in the carrier of A1 iff ( f in Funcs the carrier of S,the carrier of T & f is monotone ) ) ) & ( for f being Function of S,T holds
( f in the carrier of A2 iff ( f in Funcs the carrier of S,the carrier of T & f is monotone ) ) ) implies A1 = A2 )
assume that
A2: for f being Function of S,T holds
( f in the carrier of A1 iff ( f in Funcs the carrier of S,the carrier of T & f is monotone ) ) and
A3: for f being Function of S,T holds
( f in the carrier of A2 iff ( f in Funcs the carrier of S,the carrier of T & f is monotone ) ) ; :: thesis: A1 = A2
the carrier of A1 c= the carrier of (T |^ the carrier of S) by YELLOW_0:def 13;
then A4: the carrier of A1 c= Funcs the carrier of S,the carrier of T by Th28;
the carrier of A2 c= the carrier of (T |^ the carrier of S) by YELLOW_0:def 13;
then A5: the carrier of A2 c= Funcs the carrier of S,the carrier of T by Th28;
the carrier of A1 = the carrier of A2

proof

thus the carrier of A1 c= the carrier of A2 :: according to XBOOLE_0:def 10 :: thesis: the carrier of A2 c= the carrier of A1

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of A1 or a in the carrier of A2 )
assume A6: a in the carrier of A1 ; :: thesis: a in the carrier of A2
then reconsider f = a as Function of S,T by A4, FUNCT_2:121;
f is monotone by A2, A6;
hence a in the carrier of A2 by A3, A4, A6; :: thesis: verum

end;

thus the carrier of A2 c= the carrier of A1 :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of A2 or a in the carrier of A1 )
assume A7: a in the carrier of A2 ; :: thesis: a in the carrier of A1
then reconsider f = a as Function of S,T by A5, FUNCT_2:121;
f is monotone by A3, A7;
hence a in the carrier of A1 by A2, A5, A7; :: thesis: verum

end;

end;

hence A1 = A2 by YELLOW_0:58; :: thesis: verum