let L be lower-bounded continuous LATTICE; :: thesis: for X, Y being Subset of L st X is order-generating & X c= Y holds

Y is order-generating

let X, Y be Subset of L; :: thesis: ( X is order-generating & X c= Y implies Y is order-generating )

assume that

A1: X is order-generating and

A2: X c= Y ; :: thesis: Y is order-generating

let x be Element of L; :: according to WAYBEL_6:def 5 :: thesis: ( ex_inf_of (uparrow x) /\ Y,L & x = inf ((uparrow x) /\ Y) )

thus ex_inf_of (uparrow x) /\ Y,L by YELLOW_0:17; :: thesis: x = inf ((uparrow x) /\ Y)

A3: ex_inf_of (uparrow x) /\ Y,L by YELLOW_0:17;

ex_inf_of uparrow x,L by WAYBEL_0:39;

then inf ((uparrow x) /\ Y) >= inf (uparrow x) by A3, XBOOLE_1:17, YELLOW_0:35;

then A4: inf ((uparrow x) /\ Y) >= x by WAYBEL_0:39;

ex_inf_of (uparrow x) /\ X,L by YELLOW_0:17;

then inf ((uparrow x) /\ X) >= inf ((uparrow x) /\ Y) by A2, A3, XBOOLE_1:26, YELLOW_0:35;

then x >= inf ((uparrow x) /\ Y) by A1;

hence x = inf ((uparrow x) /\ Y) by A4, ORDERS_2:2; :: thesis: verum

Y is order-generating

let X, Y be Subset of L; :: thesis: ( X is order-generating & X c= Y implies Y is order-generating )

assume that

A1: X is order-generating and

A2: X c= Y ; :: thesis: Y is order-generating

let x be Element of L; :: according to WAYBEL_6:def 5 :: thesis: ( ex_inf_of (uparrow x) /\ Y,L & x = inf ((uparrow x) /\ Y) )

thus ex_inf_of (uparrow x) /\ Y,L by YELLOW_0:17; :: thesis: x = inf ((uparrow x) /\ Y)

A3: ex_inf_of (uparrow x) /\ Y,L by YELLOW_0:17;

ex_inf_of uparrow x,L by WAYBEL_0:39;

then inf ((uparrow x) /\ Y) >= inf (uparrow x) by A3, XBOOLE_1:17, YELLOW_0:35;

then A4: inf ((uparrow x) /\ Y) >= x by WAYBEL_0:39;

ex_inf_of (uparrow x) /\ X,L by YELLOW_0:17;

then inf ((uparrow x) /\ X) >= inf ((uparrow x) /\ Y) by A2, A3, XBOOLE_1:26, YELLOW_0:35;

then x >= inf ((uparrow x) /\ Y) by A1;

hence x = inf ((uparrow x) /\ Y) by A4, ORDERS_2:2; :: thesis: verum