let X be set ; :: thesis: for SF being Subset-Family of X
for Y being non empty Subset-Family of [:X,X:] st Y c= subbasis_Pervin_uniformity SF holds
(meet Y) ~ = meet (Y [~])
let SF be Subset-Family of X; :: thesis: for Y being non empty Subset-Family of [:X,X:] st Y c= subbasis_Pervin_uniformity SF holds
(meet Y) ~ = meet (Y [~])
let Y be non empty Subset-Family of [:X,X:]; :: thesis: ( Y c= subbasis_Pervin_uniformity SF implies (meet Y) ~ = meet (Y [~]) )
assume A1: Y c= subbasis_Pervin_uniformity SF ; :: thesis: (meet Y) ~ = meet (Y [~])
thus (meet Y) ~ c= meet (Y [~]) :: according to XBOOLE_0:def 10 :: thesis: meet (Y [~]) c= (meet Y) ~

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (meet Y) ~ or x in meet (Y [~]) )
assume A3: x in (meet Y) ~ ; :: thesis: x in meet (Y [~])
then consider a, b being object such that
a in X and
b in X and
A4: [a,b] = x by ZFMISC_1:def 2;
A5: [b,a] in meet Y by A3, A4, RELAT_1:def 7;
not Y is empty ;
then consider y being object such that
A6: y in Y ;
reconsider y = y as Element of Y by A6;
reconsider z = y as Relation of X ;
A7: y ~ in Y [~] ;

now :: thesis: for Z being set st Z in Y [~] holds
[a,b] in Z

let Z be set ; :: thesis: ( Z in Y [~] implies [a,b] in Z )
assume A8: Z in Y [~] ; :: thesis: [a,b] in Z
then A9: Z in Y by A1, Th40;
reconsider T = Z as Relation of X by A8;
T in subbasis_Pervin_uniformity SF by A9, A1;
then consider A being Element of SF such that
A10: T = block_Pervin_uniformity A ;
T ~ = T by A10, Th39;
then [b,a] in T ~ by A9, A5, SETFAM_1:def 1;
hence [a,b] in Z by RELAT_1:def 7; :: thesis: verum

end;

hence x in meet (Y [~]) by A7, A4, SETFAM_1:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet (Y [~]) or x in (meet Y) ~ )
assume A11: x in meet (Y [~]) ; :: thesis: x in (meet Y) ~
then consider a, b being object such that
a in X and
b in X and
A12: [a,b] = x by ZFMISC_1:def 2;

now :: thesis: for Z being set st Z in Y holds
[b,a] in Z

let Z be set ; :: thesis: ( Z in Y implies [b,a] in Z )
assume A13: Z in Y ; :: thesis: [b,a] in Z
then reconsider T = Z as Relation of X ;
reconsider R = T as Element of Y by A13;
R ~ = T ~ ;
then T ~ in Y [~] ;
then [a,b] in T ~ by A11, A12, SETFAM_1:def 1;
hence [b,a] in Z by RELAT_1:def 7; :: thesis: verum

end;

then [b,a] in meet Y by SETFAM_1:def 1;
hence x in (meet Y) ~ by A12, RELAT_1:def 7; :: thesis: verum