let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A3: z in X ; :: thesis:
then reconsider x1 = z as Element of X ;
reconsider x1 = x1 as Element of L by A3;
consider y being Element of L such that
A4: y in X and
A5: y << x1 by A1, A3;
x1 in { y1 where y1 is Element of L : y1 >> y } by A5;
then A6: x1 in wayabove y by WAYBEL_3:def 4;
wayabove y in { (wayabove x) where x is Element of L : x in X } by A4;
hence z in union { (wayabove x) where x is Element of L : x in X } by A6, TARSKI:def 4; :: thesis:

end;

union { (wayabove x) where x is Element of L : x in X } c= X

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in union { (wayabove x) where x is Element of L : x in X } ; :: thesis:
then consider Y being set such that
A7: z in Y and
A8: Y in { (wayabove x) where x is Element of L : x in X } by TARSKI:def 4;
consider x being Element of L such that
A9: Y = wayabove x and
A10: x in X by A8;
z in { y where y is Element of L : y >> x } by A7, A9, WAYBEL_3:def 4;
then consider z1 being Element of L such that
A11: z1 = z and
A12: z1 >> x ;
x <= z1 by A12, WAYBEL_3:1;
hence z in X by A10, A11, WAYBEL_0:def 20; :: thesis:

end;

hence X = union { (wayabove x) where x is Element of L : x in X } by A2; :: thesis:

end;

assume A13: X = union { (wayabove x) where x is Element of L : x in X } ; :: thesis:

let x1 be Element of L; :: thesis:
assume x1 in X ; :: thesis:
then consider Y being set such that
A14: x1 in Y and
A15: Y in { (wayabove x) where x is Element of L : x in X } by A13, TARSKI:def 4;
consider x being Element of L such that
A16: Y = wayabove x and
A17: x in X by A15;
x1 in { y where y is Element of L : y >> x } by A14, A16, WAYBEL_3:def 4;
then ex z1 being Element of L st
( z1 = x1 & z1 >> x ) ;
hence ex x being Element of L st
( x in X & x << x1 ) by A17; :: thesis:

end;