assume A3: y << f . x ; :: thesis: ex v being Element of S st
( v << x & y << f . v )
reconsider D = f .: (waybelow x) as non empty directed Subset of T by A1, Th13, YELLOW_2:15;
A4: f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) by A1;
A5: the carrier of S c= dom f by FUNCT_2:def 1;
defpred S₁[ Element of S] means $1 << x;
deffunc H₁( Element of S) -> Element of S = $1;
f .: { H₁(w) where w is Element of S : S₁[w] } = { (f . H₁(w)) where w is Element of S : S₁[w] } from WAYBEL17:sch 2(A5);
then consider w being Element of T such that
A6: w in D and
A7: y << w by A3, A4, WAYBEL_4:53;
consider v being object such that
A8: v in the carrier of S and
A9: v in waybelow x and
A10: w = f . v by A6, FUNCT_2:64;
reconsider v = v as Element of S by A8;
take v = v; :: thesis: ( v << x & y << f . v )
thus ( v << x & y << f . v ) by A7, A9, A10, WAYBEL_3:7; :: thesis: verum