A1: not QUS is void ;
reconsider EQUS = the entourages of QUS as Subset-Family of [: the carrier of QUS, the carrier of QUS:] ;
A10: not the entourages of (QUS [~]) is empty
proof
assume A11: the entourages of (QUS [~]) is empty ; :: thesis: contradiction
set S = the Element of the entourages of QUS;
reconsider S = the Element of the entourages of QUS as Element of the entourages of QUS ;
S ~ in the entourages of QUS [~] ;
hence contradiction by A11; :: thesis: verum
end;
for Y1, Y2 being Subset of [: the carrier of (QUS [~]), the carrier of (QUS [~]):] st Y1 in the entourages of (QUS [~]) & Y1 c= Y2 holds
Y2 in the entourages of (QUS [~])
proof
let Y1, Y2 be Subset of [: the carrier of (QUS [~]), the carrier of (QUS [~]):]; :: thesis: ( Y1 in the entourages of (QUS [~]) & Y1 c= Y2 implies Y2 in the entourages of (QUS [~]) )
assume that
A12: Y1 in the entourages of (QUS [~]) and
A13: Y1 c= Y2 ; :: thesis: Y2 in the entourages of (QUS [~])
consider U1 being Element of the entourages of QUS such that
A14: Y1 = U1 ~ by A12;
A15: Y1 ~ = U1 by A14;
QUS is upper ;
then reconsider U2 = Y2 ~ as Element of the entourages of QUS by A13, SYSREL:11, A15, CARDFIL2:def 1, A1;
consider R2 being Relation of the carrier of QUS such that
A16: Y2 = R2 and
Y2 ~ = R2 ~ ;
U2 ~ = (R2 ~) ~ by A16;
hence Y2 in the entourages of (QUS [~]) ; :: thesis: verum
end;
then the entourages of (QUS [~]) is upper ;
hence QUS [~] is upper ; :: thesis: ( QUS [~] is cap-closed & QUS [~] is axiom_U1 & QUS [~] is axiom_U3 )
for Y1, Y2 being set st Y1 in the entourages of (QUS [~]) & Y2 in the entourages of (QUS [~]) holds
Y1 /\ Y2 in the entourages of (QUS [~])
proof
let Y1, Y2 be set ; :: thesis: ( Y1 in the entourages of (QUS [~]) & Y2 in the entourages of (QUS [~]) implies Y1 /\ Y2 in the entourages of (QUS [~]) )
assume that
A17: Y1 in the entourages of (QUS [~]) and
A18: Y2 in the entourages of (QUS [~]) ; :: thesis: Y1 /\ Y2 in the entourages of (QUS [~])
consider U1 being Element of the entourages of QUS such that
A19: Y1 = U1 ~ by A17;
consider U2 being Element of the entourages of QUS such that
A20: Y2 = U2 ~ by A18;
reconsider U12 = U1 /\ U2 as Element of the entourages of QUS ;
Y1 /\ Y2 = U12 ~ by A19, A20, RELAT_1:22;
hence Y1 /\ Y2 in the entourages of (QUS [~]) ; :: thesis: verum
end;
hence QUS [~] is cap-closed by FINSUB_1:def 2; :: thesis: ( QUS [~] is axiom_U1 & QUS [~] is axiom_U3 )
thus for S being Element of the entourages of (QUS [~]) holds id the carrier of (QUS [~]) c= S :: according to UNIFORM2:def 9 :: thesis: QUS [~] is axiom_U3
proof
let S be Element of the entourages of (QUS [~]); :: thesis: id the carrier of (QUS [~]) c= S
S in { (U ~) where U is Element of the entourages of QUS : verum } by A10;
then consider U being Element of the entourages of QUS such that
A21: S = U ~ ;
QUS is axiom_U1 ;
then (id the carrier of QUS) ~ c= U ~ by SYSREL:11;
hence id the carrier of (QUS [~]) c= S by A21; :: thesis: verum
end;
thus for S being Element of the entourages of (QUS [~]) ex W being Element of the entourages of (QUS [~]) st W * W c= S :: according to UNIFORM2:def 11 :: thesis: verum
proof
let S be Element of the entourages of (QUS [~]); :: thesis: ex W being Element of the entourages of (QUS [~]) st W * W c= S
S in the entourages of (QUS [~]) by A10;
then consider U being Element of the entourages of QUS such that
A24: S = U ~ ;
QUS is axiom_U3 ;
then consider W being Element of the entourages of QUS such that
A27: W * W c= U ;
W ~ in the entourages of QUS [~] ;
then reconsider W2 = W [~] as Element of the entourages of (QUS [~]) ;
take W2 ; :: thesis: W2 * W2 c= S
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in W2 * W2 or t in S )
assume A30: t in W2 * W2 ; :: thesis: t in S
t in { [x,y] where x, y is Element of QUS : ex z being Element of QUS st
( [x,z] in W2 & [z,y] in W2 ) } by A30, Th3;
then consider x, y being Element of QUS such that
A34: t = [x,y] and
A35: ex z being Element of QUS st
( [x,z] in W2 & [z,y] in W2 ) ;
consider z being Element of QUS such that
A36: [x,z] in W2 and
A37: [z,y] in W2 by A35;
A38: [z,x] in (W ~) ~ by A36, RELAT_1:def 7;
[y,z] in (W ~) ~ by A37, RELAT_1:def 7;
then [y,x] in W * W by A38, RELAT_1:def 8;
hence t in S by A24, A34, A27, RELAT_1:def 7; :: thesis: verum
end;