let S1, S2, T1, T2 be non empty RelStr ; :: thesis: ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of T1, the InternalRel of T1 #) & RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) implies for f being Function of S1,S2

for g being Function of T1,T2 st f = g holds

for X being Subset of S1

for Y being Subset of T1 st X = Y holds

( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) ) )

assume that

A1: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of T1, the InternalRel of T1 #) and

A2: RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; :: thesis: for f being Function of S1,S2

for g being Function of T1,T2 st f = g holds

for X being Subset of S1

for Y being Subset of T1 st X = Y holds

( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) )

let f be Function of S1,S2; :: thesis: for g being Function of T1,T2 st f = g holds

for X being Subset of S1

for Y being Subset of T1 st X = Y holds

( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) )

let g be Function of T1,T2; :: thesis: ( f = g implies for X being Subset of S1

for Y being Subset of T1 st X = Y holds

( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) ) )

assume A3: f = g ; :: thesis: for X being Subset of S1

for Y being Subset of T1 st X = Y holds

( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) )

let X be Subset of S1; :: thesis: for Y being Subset of T1 st X = Y holds

( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) )

let Y be Subset of T1; :: thesis: ( X = Y implies ( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) ) )

assume A4: X = Y ; :: thesis: ( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) )

thus ( f preserves_sup_of X implies g preserves_sup_of Y ) :: thesis: ( f preserves_inf_of X implies g preserves_inf_of Y )

assume A8: ex_inf_of Y,T1 ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of g .: Y,T2 & inf (g .: Y) = g . (inf Y) )

hence ex_inf_of g .: Y,T2 by A1, A2, A3, A4, A7, YELLOW_0:14; :: thesis: inf (g .: Y) = g . (inf Y)

inf (f .: X) = inf (g .: Y) by A1, A2, A3, A4, A7, A8, YELLOW_0:14, YELLOW_0:27;

hence inf (g .: Y) = g . (inf Y) by A1, A3, A4, A7, A8, YELLOW_0:14, YELLOW_0:27; :: thesis: verum

for g being Function of T1,T2 st f = g holds

for X being Subset of S1

for Y being Subset of T1 st X = Y holds

( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) ) )

assume that

A1: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of T1, the InternalRel of T1 #) and

A2: RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; :: thesis: for f being Function of S1,S2

for g being Function of T1,T2 st f = g holds

for X being Subset of S1

for Y being Subset of T1 st X = Y holds

( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) )

let f be Function of S1,S2; :: thesis: for g being Function of T1,T2 st f = g holds

for X being Subset of S1

for Y being Subset of T1 st X = Y holds

( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) )

let g be Function of T1,T2; :: thesis: ( f = g implies for X being Subset of S1

for Y being Subset of T1 st X = Y holds

( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) ) )

assume A3: f = g ; :: thesis: for X being Subset of S1

for Y being Subset of T1 st X = Y holds

( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) )

let X be Subset of S1; :: thesis: for Y being Subset of T1 st X = Y holds

( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) )

let Y be Subset of T1; :: thesis: ( X = Y implies ( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) ) )

assume A4: X = Y ; :: thesis: ( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) )

thus ( f preserves_sup_of X implies g preserves_sup_of Y ) :: thesis: ( f preserves_inf_of X implies g preserves_inf_of Y )

proof

assume A7:
( ex_inf_of X,S1 implies ( ex_inf_of f .: X,S2 & inf (f .: X) = f . (inf X) ) )
; :: according to WAYBEL_0:def 30 :: thesis: g preserves_inf_of Y
assume A5:
( ex_sup_of X,S1 implies ( ex_sup_of f .: X,S2 & sup (f .: X) = f . (sup X) ) )
; :: according to WAYBEL_0:def 31 :: thesis: g preserves_sup_of Y

assume A6: ex_sup_of Y,T1 ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of g .: Y,T2 & sup (g .: Y) = g . (sup Y) )

hence ex_sup_of g .: Y,T2 by A1, A2, A3, A4, A5, YELLOW_0:14; :: thesis: sup (g .: Y) = g . (sup Y)

sup (f .: X) = sup (g .: Y) by A1, A2, A3, A4, A5, A6, YELLOW_0:14, YELLOW_0:26;

hence sup (g .: Y) = g . (sup Y) by A1, A3, A4, A5, A6, YELLOW_0:14, YELLOW_0:26; :: thesis: verum

end;assume A6: ex_sup_of Y,T1 ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of g .: Y,T2 & sup (g .: Y) = g . (sup Y) )

hence ex_sup_of g .: Y,T2 by A1, A2, A3, A4, A5, YELLOW_0:14; :: thesis: sup (g .: Y) = g . (sup Y)

sup (f .: X) = sup (g .: Y) by A1, A2, A3, A4, A5, A6, YELLOW_0:14, YELLOW_0:26;

hence sup (g .: Y) = g . (sup Y) by A1, A3, A4, A5, A6, YELLOW_0:14, YELLOW_0:26; :: thesis: verum

assume A8: ex_inf_of Y,T1 ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of g .: Y,T2 & inf (g .: Y) = g . (inf Y) )

hence ex_inf_of g .: Y,T2 by A1, A2, A3, A4, A7, YELLOW_0:14; :: thesis: inf (g .: Y) = g . (inf Y)

inf (f .: X) = inf (g .: Y) by A1, A2, A3, A4, A7, A8, YELLOW_0:14, YELLOW_0:27;

hence inf (g .: Y) = g . (inf Y) by A1, A3, A4, A7, A8, YELLOW_0:14, YELLOW_0:27; :: thesis: verum