let T be non empty TopSpace; :: thesis: for L1 being lower-bounded continuous LATTICE st InclPoset the topology of T = L1 holds
for B1 being Basis of T
for B2 being Subset of L1 st B1 = B2 holds
finsups B2 is with_bottom CLbasis of L1
let L1 be lower-bounded continuous LATTICE; :: thesis: ( InclPoset the topology of T = L1 implies for B1 being Basis of T
for B2 being Subset of L1 st B1 = B2 holds
finsups B2 is with_bottom CLbasis of L1 )
assume A1:
InclPoset the topology of T = L1
; :: thesis: for B1 being Basis of T
for B2 being Subset of L1 st B1 = B2 holds
finsups B2 is with_bottom CLbasis of L1
let B1 be Basis of T; :: thesis: for B2 being Subset of L1 st B1 = B2 holds
finsups B2 is with_bottom CLbasis of L1
let B2 be Subset of L1; :: thesis: ( B1 = B2 implies finsups B2 is with_bottom CLbasis of L1 )
assume A2:
B1 = B2
; :: thesis: finsups B2 is with_bottom CLbasis of L1
now let x,
y be
Element of
L1;
:: thesis: ( x in finsups B2 & y in finsups B2 implies sup {x,y} in finsups B2 )assume that A3:
x in finsups B2
and A4:
y in finsups B2
;
:: thesis: sup {x,y} in finsups B2
x in { ("\/" Y,L1) where Y is finite Subset of B2 : ex_sup_of Y,L1 }
by A3, WAYBEL_0:def 27;
then consider Y1 being
finite Subset of
B2 such that A5:
x = "\/" Y1,
L1
and A6:
ex_sup_of Y1,
L1
;
y in { ("\/" Y,L1) where Y is finite Subset of B2 : ex_sup_of Y,L1 }
by A4, WAYBEL_0:def 27;
then consider Y2 being
finite Subset of
B2 such that A7:
y = "\/" Y2,
L1
and A8:
ex_sup_of Y2,
L1
;
(
ex_sup_of Y1 \/ Y2,
L1 &
"\/" (Y1 \/ Y2),
L1 = ("\/" Y1,L1) "\/" ("\/" Y2,L1) )
by A6, A8, YELLOW_2:3;
then
x "\/" y in { ("\/" Y,L1) where Y is finite Subset of B2 : ex_sup_of Y,L1 }
by A5, A7;
then
x "\/" y in finsups B2
by WAYBEL_0:def 27;
hence
sup {x,y} in finsups B2
by YELLOW_0:41;
:: thesis: verum end;
then A9:
finsups B2 is join-closed
by WAYBEL23:18;
( {} c= B2 & ex_sup_of {} ,L1 )
by XBOOLE_1:2, YELLOW_0:42;
then
"\/" {} ,L1 in { ("\/" Y,L1) where Y is finite Subset of B2 : ex_sup_of Y,L1 }
;
then A10:
Bottom L1 in finsups B2
by WAYBEL_0:def 27;
for x, y being Element of L1 st not y <= x holds
ex b being Element of L1 st
( b in finsups B2 & not b <= x & b <= y )
proof
let x,
y be
Element of
L1;
:: thesis: ( not y <= x implies ex b being Element of L1 st
( b in finsups B2 & not b <= x & b <= y ) )
(
x in the
carrier of
L1 &
y in the
carrier of
L1 )
;
then A11:
(
x in the
topology of
T &
y in the
topology of
T )
by A1, YELLOW_1:1;
then reconsider y1 =
y as
Subset of
T ;
assume
not
y <= x
;
:: thesis: ex b being Element of L1 st
( b in finsups B2 & not b <= x & b <= y )
then
not
y c= x
by A1, YELLOW_1:3;
then consider v being
set such that A12:
v in y
and A13:
not
v in x
by TARSKI:def 3;
v in y1
by A12;
then reconsider v =
v as
Point of
T ;
y1 is
open
by A11, PRE_TOPC:def 5;
then consider b being
Subset of
T such that A14:
b in B1
and A15:
v in b
and A16:
b c= y1
by A12, YELLOW_9:31;
reconsider b =
b as
Element of
L1 by A2, A14;
take
b
;
:: thesis: ( b in finsups B2 & not b <= x & b <= y )
for
z being
set st
z in {b} holds
z in B2
by A2, A14, TARSKI:def 1;
then A17:
{b} is
finite Subset of
B2
by TARSKI:def 3;
A18:
ex_sup_of {b},
L1
by YELLOW_0:38;
b = "\/" {b},
L1
by YELLOW_0:39;
then
b in { ("\/" Y,L1) where Y is finite Subset of B2 : ex_sup_of Y,L1 }
by A17, A18;
hence
b in finsups B2
by WAYBEL_0:def 27;
:: thesis: ( not b <= x & b <= y )
not
b c= x
by A13, A15;
hence
not
b <= x
by A1, YELLOW_1:3;
:: thesis: b <= y
thus
b <= y
by A1, A16, YELLOW_1:3;
:: thesis: verum
end;
hence
finsups B2 is with_bottom CLbasis of L1
by A9, A10, WAYBEL23:49, WAYBEL23:def 8; :: thesis: verum