let S, T be non empty RelStr ; :: thesis: for A being Subset of S
for f being Function of S,T st f is isomorphic & ex_sup_of A,S holds
ex_sup_of f .: A,T
let A be Subset of S; :: thesis: for f being Function of S,T st f is isomorphic & ex_sup_of A,S holds
ex_sup_of f .: A,T
let f be Function of S,T; :: thesis: ( f is isomorphic & ex_sup_of A,S implies ex_sup_of f .: A,T )
assume A1: f is isomorphic ; :: thesis: ( not ex_sup_of A,S or ex_sup_of f .: A,T )
given a being Element of S such that A2: A is_<=_than a and
A3: for b being Element of S st A is_<=_than b holds
b >= a and
A4: for c being Element of S st A is_<=_than c & ( for b being Element of S st A is_<=_than b holds
b >= c ) holds
c = a ; :: according to YELLOW_0:def 7 :: thesis: ex_sup_of f .: A,T
A5: f /" is isomorphic by A1, Th11;
A6: ( f is one-to-one & rng f = [#] T ) by A1, WAYBEL_0:66;
then A7: f /" = f " by TOPS_2:def 4;
take f . a ; :: according to YELLOW_0:def 7 :: thesis: ( f .: A is_<=_than f . a & ( for b₁ being Element of the carrier of T holds
( not f .: A is_<=_than b₁ or f . a <= b₁ ) ) & ( for b₁ being Element of the carrier of T holds
( not f .: A is_<=_than b₁ or ex b₂ being Element of the carrier of T st
( f .: A is_<=_than b₂ & not b₁ <= b₂ ) or b₁ = f . a ) ) )
thus f .: A is_<=_than f . a by A1, A2, WAYBEL13:19; :: thesis: ( ( for b₁ being Element of the carrier of T holds
( not f .: A is_<=_than b₁ or f . a <= b₁ ) ) & ( for b₁ being Element of the carrier of T holds
( not f .: A is_<=_than b₁ or ex b₂ being Element of the carrier of T st
( f .: A is_<=_than b₂ & not b₁ <= b₂ ) or b₁ = f . a ) ) )
A8: dom f = the carrier of S by FUNCT_2:def 1;
A9: f " (f .: A) = A

proof

thus f " (f .: A) c= A by A6, FUNCT_1:152; :: according to XBOOLE_0:def 10 :: thesis: A c= f " (f .: A)
thus A c= f " (f .: A) by A8, FUNCT_1:146; :: thesis: verum

end;

hereby :: thesis: for b₁ being Element of the carrier of T holds
( not f .: A is_<=_than b₁ or ex b₂ being Element of the carrier of T st
( f .: A is_<=_than b₂ & not b₁ <= b₂ ) or b₁ = f . a )

let b be Element of T; :: thesis: ( f .: A is_<=_than b implies b >= f . a )
assume f .: A is_<=_than b ; :: thesis: b >= f . a
then (f /" ) .: (f .: A) is_<=_than (f /" ) . b by A5, WAYBEL13:19;
then f " (f .: A) is_<=_than (f /" ) . b by A6, TOPS_2:68;
then (f /" ) . b >= a by A3, A9;
then f . ((f /" ) . b) >= f . a by A1, WAYBEL_0:66;
hence b >= f . a by A6, A7, FUNCT_1:57; :: thesis: verum

end;

let c be Element of T; :: thesis: ( not f .: A is_<=_than c or ex b₁ being Element of the carrier of T st
( f .: A is_<=_than b₁ & not c <= b₁ ) or c = f . a )
assume f .: A is_<=_than c ; :: thesis: ( ex b₁ being Element of the carrier of T st
( f .: A is_<=_than b₁ & not c <= b₁ ) or c = f . a )
then (f /" ) .: (f .: A) is_<=_than (f /" ) . c by A5, WAYBEL13:19;
then A10: A is_<=_than (f /" ) . c by A6, A9, TOPS_2:68;
assume A11: for b being Element of T st f .: A is_<=_than b holds
b >= c ; :: thesis: c = f . a
for b being Element of S st A is_<=_than b holds
b >= (f /" ) . c

proof

let b be Element of S; :: thesis: ( A is_<=_than b implies b >= (f /" ) . c )
assume A is_<=_than b ; :: thesis: b >= (f /" ) . c
then f .: A is_<=_than f . b by A1, WAYBEL13:19;
then f . b >= c by A11;
then (f /" ) . (f . b) >= (f /" ) . c by A5, WAYBEL_0:66;
hence b >= (f /" ) . c by A6, A7, A8, FUNCT_1:56; :: thesis: verum

end;

then (f /" ) . c = a by A4, A10;
hence c = f . a by A6, A7, FUNCT_1:57; :: thesis: verum