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 set such that
A3: ( a in the carrier of S & a in X & x = f . a ) by FUNCT_2:115;
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 set such that
A4: ( b in the carrier of S & b in X & y = f . b ) by FUNCT_2:115;
reconsider a = a, b = b as Element of S by A3, A4;
consider c being Element of S such that
A5: ( c in X & c <= a & c <= b ) by A2, A3, A4, WAYBEL_0:def 2;
take z = f . c; :: thesis: ( z in f .: X & z <= x & z <= y )
thus z in f .: X by A5, FUNCT_2:43; :: thesis: ( z <= x & z <= y )
thus ( z <= x & z <= y ) by A1, A3, A4, A5, WAYBEL_1:def 2; :: thesis: verum