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
A1: 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
A2: 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 A2 c= the carrier of (T |^ the carrier of S) by YELLOW_0:def 13;
then A3: the carrier of A2 c= Funcs ( the carrier of S, the carrier of T) by Th28;
A4: the carrier of A2 c= the carrier of A1

proof

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

end;

the carrier of A1 c= the carrier of (T |^ the carrier of S) by YELLOW_0:def 13;
then A6: the carrier of A1 c= Funcs ( the carrier of S, the carrier of T) by Th28;
the carrier of A1 c= the carrier of A2

proof

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

end;

then the carrier of A1 = the carrier of A2 by A4;
hence A1 = A2 by YELLOW_0:57; :: thesis: verum