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_inf_of A,S holds
ex_inf_of f .: A,T
let A be Subset of S; :: thesis: for f being Function of S,T st f is isomorphic & ex_inf_of A,S holds
ex_inf_of f .: A,T
let f be Function of S,T; :: thesis: ( f is isomorphic & ex_inf_of A,S implies ex_inf_of f .: A,T )
assume A1: f is isomorphic ; :: thesis: ( not ex_inf_of A,S or ex_inf_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 8 :: thesis: ex_inf_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 8 :: thesis: ( f . a is_<=_than f .: A & ( for b₁ being Element of the carrier of T holds
( not b₁ is_<=_than f .: A or b₁ <= f . a ) ) & ( for b₁ being Element of the carrier of T holds
( not b₁ is_<=_than f .: A or ex b₂ being Element of the carrier of T st
( b₂ is_<=_than f .: A & not b₂ <= b₁ ) or b₁ = f . a ) ) )
thus f .: A is_>=_than f . a by A1, A2, WAYBEL13:18; :: thesis: ( ( for b₁ being Element of the carrier of T holds
( not b₁ is_<=_than f .: A or b₁ <= f . a ) ) & ( for b₁ being Element of the carrier of T holds
( not b₁ is_<=_than f .: A or ex b₂ being Element of the carrier of T st
( b₂ is_<=_than f .: A & 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 b₁ is_<=_than f .: A or ex b₂ being Element of the carrier of T st
( b₂ is_<=_than f .: A & 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:18;
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 c is_<=_than f .: A or ex b₁ being Element of the carrier of T st
( b₁ is_<=_than f .: A & not b₁ <= c ) or c = f . a )
assume f .: A is_>=_than c ; :: thesis: ( ex b₁ being Element of the carrier of T st
( b₁ is_<=_than f .: A & not b₁ <= c ) or c = f . a )
then (f /" ) .: (f .: A) is_>=_than (f /" ) . c by A5, WAYBEL13:18;
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:18;
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