let S, T be non empty RelStr ; :: thesis: ( S,T are_isomorphic & S is with_infima implies T is with_infima )
given f being Function of S,T such that A1: f is isomorphic ; :: according to WAYBEL_1:def 8 :: thesis: ( not S is with_infima or T is with_infima )
assume A2: for a, b being Element of S ex c being Element of S st
( c <= a & c <= b & ( for c9 being Element of S st c9 <= a & c9 <= b holds
c9 <= c ) ) ; :: according to LATTICE3:def 11 :: thesis: T is with_infima
let x, y be Element of T; :: according to LATTICE3:def 11 :: thesis: ex b₁ being Element of the carrier of T st
( b₁ <= x & b₁ <= y & ( for b₂ being Element of the carrier of T holds
( not b₂ <= x or not b₂ <= y or b₂ <= b₁ ) ) )
consider c being Element of S such that
A3: ( c <= (f /") . x & c <= (f /") . y ) and
A4: for c9 being Element of S st c9 <= (f /") . x & c9 <= (f /") . y holds
c9 <= c by A2;
take f . c ; :: thesis: ( f . c <= x & f . c <= y & ( for b₁ being Element of the carrier of T holds
( not b₁ <= x or not b₁ <= y or b₁ <= f . c ) ) )
A5: ex g being Function of T,S st
( g = f " & g is monotone ) by A1, WAYBEL_0:def 38;
A6: rng f = the carrier of T by A1, WAYBEL_0:66;
A7: f /" = f " by A1, TOPS_2:def 4;
( f . c <= f . ((f /") . x) & f . c <= f . ((f /") . y) ) by A1, A3, WAYBEL_0:66;
hence ( f . c <= x & f . c <= y ) by A1, A6, A7, FUNCT_1:35; :: thesis: for b₁ being Element of the carrier of T holds
( not b₁ <= x or not b₁ <= y or b₁ <= f . c )
let z9 be Element of T; :: thesis: ( not z9 <= x or not z9 <= y or z9 <= f . c )
assume ( z9 <= x & z9 <= y ) ; :: thesis: z9 <= f . c
then ( (f /") . z9 <= (f /") . x & (f /") . z9 <= (f /") . y ) by A7, A5, WAYBEL_1:def 2;
then (f /") . z9 <= c by A4;
then f . ((f /") . z9) <= f . c by A1, WAYBEL_0:66;
hence z9 <= f . c by A1, A6, A7, FUNCT_1:35; :: thesis: verum