let S1, S2, T1, T2 be non empty RelStr ; ( 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 #)
; 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; 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; ( 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
; 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; 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; ( 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
; ( ( 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 )
( f preserves_inf_of X implies g preserves_inf_of Y )proof
assume A5:
(
ex_sup_of X,
S1 implies (
ex_sup_of f .: X,
S2 &
sup (f .: X) = f . (sup X) ) )
;
WAYBEL_0:def 31 g preserves_sup_of Y
assume A6:
ex_sup_of Y,
T1
;
WAYBEL_0:def 31 ( 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;
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;
verum
end;
assume A7:
( ex_inf_of X,S1 implies ( ex_inf_of f .: X,S2 & inf (f .: X) = f . (inf X) ) )
; WAYBEL_0:def 30 g preserves_inf_of Y
assume A8:
ex_inf_of Y,T1
; WAYBEL_0:def 30 ( 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; 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; verum