let X be set ; for cB being Subset-Family of [:X,X:] st cB is quasi_basis & cB is axiom_UP1 & cB is axiom_UP3 holds
UniformSpaceStr(# X,<.cB.] #) is Quasi-UniformSpace
let cB be Subset-Family of [:X,X:]; ( cB is quasi_basis & cB is axiom_UP1 & cB is axiom_UP3 implies UniformSpaceStr(# X,<.cB.] #) is Quasi-UniformSpace )
assume that
A1:
cB is quasi_basis
and
A2:
cB is axiom_UP1
and
A4:
cB is axiom_UP3
; UniformSpaceStr(# X,<.cB.] #) is Quasi-UniformSpace
set US = UniformSpaceStr(# X,<.cB.] #);
A5:
<.cB.] = { x where x is Subset of [:X,X:] : ex b being Element of cB st b c= x }
by CARDFIL2:14;
now ( UniformSpaceStr(# X,<.cB.] #) is upper & UniformSpaceStr(# X,<.cB.] #) is cap-closed & UniformSpaceStr(# X,<.cB.] #) is axiom_U1 & UniformSpaceStr(# X,<.cB.] #) is axiom_U3 )
for
Y1,
Y2 being
Subset of
[:X,X:] st
Y1 in <.cB.] &
Y1 c= Y2 holds
Y2 in <.cB.]
then
<.cB.] is
upper
;
hence
UniformSpaceStr(#
X,
<.cB.] #) is
upper
;
( UniformSpaceStr(# X,<.cB.] #) is cap-closed & UniformSpaceStr(# X,<.cB.] #) is axiom_U1 & UniformSpaceStr(# X,<.cB.] #) is axiom_U3 )
for
Y1,
Y2 being
set st
Y1 in <.cB.] &
Y2 in <.cB.] holds
Y1 /\ Y2 in <.cB.]
proof
let Y1,
Y2 be
set ;
( Y1 in <.cB.] & Y2 in <.cB.] implies Y1 /\ Y2 in <.cB.] )
assume that A11:
Y1 in <.cB.]
and A12:
Y2 in <.cB.]
;
Y1 /\ Y2 in <.cB.]
consider x being
Subset of
[:X,X:] such that A13:
Y1 = x
and A14:
ex
b being
Element of
cB st
b c= x
by A5, A11;
consider B1 being
Element of
cB such that A15:
B1 c= x
by A14;
Y2 in { x where x is Subset of [:X,X:] : ex b being Element of cB st b c= x }
by CARDFIL2:14, A12;
then consider y being
Subset of
[:X,X:] such that A16:
Y2 = y
and A17:
ex
b being
Element of
cB st
b c= y
;
consider B2 being
Element of
cB such that A18:
B2 c= y
by A17;
A19:
B1 /\ B2 c= Y1 /\ Y2
by A13, A15, A18, A16, XBOOLE_1:27;
consider B3 being
Element of
cB such that A20:
B3 c= B1 /\ B2
by A1;
A21:
Y1 /\ Y2 c= [:X,X:] /\ [:X,X:]
by A11, A12, XBOOLE_1:27;
B3 c= Y1 /\ Y2
by A20, A19;
hence
Y1 /\ Y2 in <.cB.]
by A5, A21;
verum
end; hence
UniformSpaceStr(#
X,
<.cB.] #) is
cap-closed
by FINSUB_1:def 2;
( UniformSpaceStr(# X,<.cB.] #) is axiom_U1 & UniformSpaceStr(# X,<.cB.] #) is axiom_U3 )
for
S being
Element of
<.cB.] holds
id X c= S
hence
UniformSpaceStr(#
X,
<.cB.] #) is
axiom_U1
;
UniformSpaceStr(# X,<.cB.] #) is axiom_U3
for
S being
Element of the
entourages of
UniformSpaceStr(#
X,
<.cB.] #) ex
W being
Element of the
entourages of
UniformSpaceStr(#
X,
<.cB.] #) st
W * W c= S
hence
UniformSpaceStr(#
X,
<.cB.] #) is
axiom_U3
;
verum end;
hence
UniformSpaceStr(# X,<.cB.] #) is Quasi-UniformSpace
; verum