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