let S1, T1, S2, T2 be non empty RelStr ; :: thesis: ( RelStr(# the carrier of S1,the InternalRel of S1 #) = RelStr(# the carrier of S2,the InternalRel of S2 #) & RelStr(# the carrier of T1,the InternalRel of T1 #) = RelStr(# the carrier of T2,the InternalRel of T2 #) implies for f1 being Function of S1,T1
for f2 being Function of S2,T2 st f1 = f2 holds
( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) ) )
assume A1: ( RelStr(# the carrier of S1,the InternalRel of S1 #) = RelStr(# the carrier of S2,the InternalRel of S2 #) & RelStr(# the carrier of T1,the InternalRel of T1 #) = RelStr(# the carrier of T2,the InternalRel of T2 #) ) ; :: thesis: for f1 being Function of S1,T1
for f2 being Function of S2,T2 st f1 = f2 holds
( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) )
let f1 be Function of S1,T1; :: thesis: for f2 being Function of S2,T2 st f1 = f2 holds
( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) )
let f2 be Function of S2,T2; :: thesis: ( f1 = f2 implies ( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) ) )
assume A2: f1 = f2 ; :: thesis: ( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) )
thus ( f1 is sups-preserving implies f2 is sups-preserving ) :: thesis: ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving )

proof

assume A3: for X being Subset of S1 holds f1 preserves_sup_of X ; :: according to WAYBEL_0:def 33 :: thesis: f2 is sups-preserving
let X be Subset of S2; :: according to WAYBEL_0:def 33 :: thesis: f2 preserves_sup_of X
reconsider Y = X as Subset of S1 by A1;
f1 preserves_sup_of Y by A3;
hence f2 preserves_sup_of X by A1, A2, WAYBEL_0:65; :: thesis: verum

end;

assume A4: for X being Subset of S1 st not X is empty & X is filtered holds
f1 preserves_inf_of X ; :: according to WAYBEL_0:def 36 :: thesis: f2 is filtered-infs-preserving
let X be Subset of S2; :: according to WAYBEL_0:def 36 :: thesis: ( X is empty or not X is filtered or f2 preserves_inf_of X )
reconsider Y = X as Subset of S1 by A1;
assume ( not X is empty & X is filtered ) ; :: thesis: f2 preserves_inf_of X
then f1 preserves_inf_of Y by A1, A4, WAYBEL_0:4;
hence f2 preserves_inf_of X by A1, A2, WAYBEL_0:65; :: thesis: verum