let S, T be RelStr ; :: thesis: for K, L being non empty RelStr
for f being Function of S,T
for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is antitone holds
g is antitone
let K, L be non empty RelStr ; :: thesis: for f being Function of S,T
for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is antitone holds
g is antitone
let f be Function of S,T; :: thesis: for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is antitone holds
g is antitone
let g be Function of K,L; :: thesis: ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is antitone implies g is antitone )
assume that
A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) and
A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) and
A3: f = g and
A4: f is antitone ; :: thesis: g is antitone
reconsider S1 = S, T1 = T as non empty RelStr by A1, A2;
let x, y be Element of K; :: according to WAYBEL_9:def 1 :: thesis: ( x <= y implies g . x >= g . y )
assume A5: x <= y ; :: thesis: g . x >= g . y
reconsider x1 = x, y1 = y as Element of S1 by A1;
reconsider f1 = f as Function of S1,T1 ;
x1 <= y1 by A1, A5;
then f1 . x1 >= f1 . y1 by A4;
hence g . x >= g . y by A2, A3; :: thesis: verum