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 )
proof
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 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 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