let T be TopSpace; :: thesis: for QU being non void Quasi-UniformSpace st the carrier of T = the carrier of QU & subbasis_Pervin_quasi_uniformity T c= the entourages of QU holds
the entourages of (Pervin_quasi_uniformity T) c= the entourages of QU
let QU be non void Quasi-UniformSpace; :: thesis: ( the carrier of T = the carrier of QU & subbasis_Pervin_quasi_uniformity T c= the entourages of QU implies the entourages of (Pervin_quasi_uniformity T) c= the entourages of QU )
assume that
A2: the carrier of T = the carrier of QU and
A3: subbasis_Pervin_quasi_uniformity T c= the entourages of QU ; :: thesis: the entourages of (Pervin_quasi_uniformity T) c= the entourages of QU
the entourages of (Pervin_quasi_uniformity T) c= the entourages of QU
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the entourages of (Pervin_quasi_uniformity T) or x in the entourages of QU )
assume A4: x in the entourages of (Pervin_quasi_uniformity T) ; :: thesis: x in the entourages of QU
then reconsider y = x as Subset of [: the carrier of T, the carrier of T:] ;
consider b being Element of basis_Pervin_quasi_uniformity T such that
A5: b c= y by A4, CARDFIL2:def 8;
b in FinMeetCl (subbasis_Pervin_quasi_uniformity T) ;
then consider Y being Subset-Family of [: the carrier of T, the carrier of T:] such that
A6: Y c= subbasis_Pervin_quasi_uniformity T and
A7: Y is finite and
A8: b = Intersect Y by CANTOR_1:def 3;
reconsider Z = Y as finite Subset-Family of [: the carrier of QU, the carrier of QU:] by A2, A7;
reconsider B = the entourages of QU as set ;
A9: now :: thesis: ( B is Subset-Family of [: the carrier of QU, the carrier of QU:] & B is cap-closed & [: the carrier of QU, the carrier of QU:] in B & Z c= B )
thus B is Subset-Family of [: the carrier of QU, the carrier of QU:] ; :: thesis: ( B is cap-closed & [: the carrier of QU, the carrier of QU:] in B & Z c= B )
QU is cap-closed ;
hence B is cap-closed ; :: thesis: ( [: the carrier of QU, the carrier of QU:] in B & Z c= B )
thus [: the carrier of QU, the carrier of QU:] in B by Th27; :: thesis: Z c= B
thus Z c= B by A3, A6; :: thesis: verum
end;
QU is upper ;
then A10: the entourages of QU is upper ;
( b is Subset of [: the carrier of QU, the carrier of QU:] & y is Subset of [: the carrier of QU, the carrier of QU:] & b c= y & b in the entourages of QU ) by A5, A9, A2, A8, ARMSTRNG:1;
hence x in the entourages of QU by A10; :: thesis: verum
end;
hence the entourages of (Pervin_quasi_uniformity T) c= the entourages of QU ; :: thesis: verum