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 ex c being Element of st
( c <= a & c <= b & ( for c' being Element of st c' <= a & c' <= b holds
c' <= c ) ) ; :: according to LATTICE3:def 11 :: thesis: T is with_infima
let x, y be Element of ; :: 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 such that
A3: ( c <= (f /" ) . x & c <= (f /" ) . y ) and
A4: for c' being Element of st c' <= (f /" ) . x & c' <= (f /" ) . y holds
c' <= 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;
then 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:57; :: thesis: for b₁ being Element of the carrier of T holds
( not b₁ <= x or not b₁ <= y or b₁ <= f . c )
let z' be Element of ; :: thesis: ( not z' <= x or not z' <= y or z' <= f . c )
assume ( z' <= x & z' <= y ) ; :: thesis: z' <= f . c
then ( (f /" ) . z' <= (f /" ) . x & (f /" ) . z' <= (f /" ) . y ) by A7, A5, WAYBEL_1:def 2;
then (f /" ) . z' <= c by A4;
then f . ((f /" ) . z') <= f . c by A1, WAYBEL_0:66;
hence z' <= f . c by A1, A6, A7, FUNCT_1:57; :: thesis: verum