let S, T be non empty RelStr ; 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; 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; ( f is isomorphic & ex_sup_of A,S implies ex_sup_of f .: A,T )
assume A1:
f is isomorphic
; ( not ex_sup_of A,S or ex_sup_of f .: A,T )
A2:
f " (f .: A) c= A
by A1, FUNCT_1:82;
A3:
rng f = [#] T
by A1, WAYBEL_0:66;
A4:
f /" = f "
by A1, TOPS_2:def 4;
given a being Element of S such that A5:
A is_<=_than a
and
A6:
for b being Element of S st A is_<=_than b holds
b >= a
and
A7:
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
; YELLOW_0:def 7 ex_sup_of f .: A,T
take
f . a
; YELLOW_0:def 7 ( f .: A is_<=_than f . a & ( for b1 being Element of the carrier of T holds
( not f .: A is_<=_than b1 or f . a <= b1 ) ) & ( for b1 being Element of the carrier of T holds
( not f .: A is_<=_than b1 or ex b2 being Element of the carrier of T st
( f .: A is_<=_than b2 & not b1 <= b2 ) or b1 = f . a ) ) )
thus
f .: A is_<=_than f . a
by A1, A5, WAYBEL13:19; ( ( for b1 being Element of the carrier of T holds
( not f .: A is_<=_than b1 or f . a <= b1 ) ) & ( for b1 being Element of the carrier of T holds
( not f .: A is_<=_than b1 or ex b2 being Element of the carrier of T st
( f .: A is_<=_than b2 & not b1 <= b2 ) or b1 = f . a ) ) )
A8:
f /" is isomorphic
by A1, Th10;
A9:
dom f = the carrier of S
by FUNCT_2:def 1;
then
A c= f " (f .: A)
by FUNCT_1:76;
then A10:
f " (f .: A) = A
by A2;
let c be Element of T; ( not f .: A is_<=_than c or ex b1 being Element of the carrier of T st
( f .: A is_<=_than b1 & not c <= b1 ) or c = f . a )
assume A11:
f .: A is_<=_than c
; ( ex b1 being Element of the carrier of T st
( f .: A is_<=_than b1 & not c <= b1 ) or c = f . a )
assume A12:
for b being Element of T st f .: A is_<=_than b holds
b >= c
; c = f . a
A13:
for b being Element of S st A is_<=_than b holds
b >= (f /") . c
(f /") .: (f .: A) is_<=_than (f /") . c
by A8, A11, WAYBEL13:19;
then
A is_<=_than (f /") . c
by A1, A3, A10, TOPS_2:55;
then
(f /") . c = a
by A7, A13;
hence
c = f . a
by A1, A3, A4, FUNCT_1:35; verum