let S, T be non empty RelStr ; :: thesis: for f being Function of S,T st f is monotone holds
for X being Subset of S st X is filtered holds
f .: X is filtered
let f be Function of S,T; :: thesis: ( f is monotone implies for X being Subset of S st X is filtered holds
f .: X is filtered )
assume A1: f is monotone ; :: thesis: for X being Subset of S st X is filtered holds
f .: X is filtered
let X be Subset of S; :: thesis: ( X is filtered implies f .: X is filtered )
assume A2: X is filtered ; :: thesis: f .: X is filtered
let x, y be Element of T; :: according to WAYBEL_0:def 2 :: thesis: ( not x in f .: X or not y in f .: X or ex b₁ being Element of the carrier of T st
( b₁ in f .: X & b₁ <= x & b₁ <= y ) )
assume x in f .: X ; :: thesis: ( not y in f .: X or ex b₁ being Element of the carrier of T st
( b₁ in f .: X & b₁ <= x & b₁ <= y ) )
then consider a being object such that
A3: a in the carrier of S and
A4: a in X and
A5: x = f . a by FUNCT_2:64;
assume y in f .: X ; :: thesis: ex b₁ being Element of the carrier of T st
( b₁ in f .: X & b₁ <= x & b₁ <= y )
then consider b being object such that
A6: b in the carrier of S and
A7: b in X and
A8: y = f . b by FUNCT_2:64;
reconsider a = a, b = b as Element of S by A3, A6;
consider c being Element of S such that
A9: c in X and
A10: ( c <= a & c <= b ) by A2, A4, A7;
take z = f . c; :: thesis: ( z in f .: X & z <= x & z <= y )
thus z in f .: X by A9, FUNCT_2:35; :: thesis: ( z <= x & z <= y )
thus ( z <= x & z <= y ) by A1, A5, A8, A10; :: thesis: verum