let X be empty set ; :: thesis: for cB being empty Subset-Family of [:X,X:] holds
( cB is quasi_basis & cB is axiom_UP1 & cB is axiom_UP2 & cB is axiom_UP3 )
let cB be empty Subset-Family of [:X,X:]; :: thesis: ( cB is quasi_basis & cB is axiom_UP1 & cB is axiom_UP2 & cB is axiom_UP3 )
for B1, B2 being Element of cB ex B being Element of cB st B c= B1 /\ B2
proof
let B1, B2 be Element of cB; :: thesis: ex B being Element of cB st B c= B1 /\ B2
reconsider B = {} as Element of cB by SUBSET_1:def 1;
take B ; :: thesis: B c= B1 /\ B2
thus B c= B1 /\ B2 ; :: thesis: verum
end;
hence cB is quasi_basis ; :: thesis: ( cB is axiom_UP1 & cB is axiom_UP2 & cB is axiom_UP3 )
for B being Element of cB holds id X c= B ;
hence cB is axiom_UP1 ; :: thesis: ( cB is axiom_UP2 & cB is axiom_UP3 )
for B1 being Element of cB ex B2 being Element of cB st B2 c= B1 ~
proof
let B1 be Element of cB; :: thesis: ex B2 being Element of cB st B2 c= B1 ~
reconsider B2 = {} as Element of cB by SUBSET_1:def 1;
B2 c= B1 ~ ;
hence ex B2 being Element of cB st B2 c= B1 ~ ; :: thesis: verum
end;
hence cB is axiom_UP2 ; :: thesis: cB is axiom_UP3
for B1 being Element of cB ex B2 being Element of cB st B2 * B2 c= B1
proof
let B1 be Element of cB; :: thesis: ex B2 being Element of cB st B2 * B2 c= B1
reconsider B2 = {} as Element of cB by SUBSET_1:def 1;
B2 * B2 c= B1 ;
hence ex B2 being Element of cB st B2 * B2 c= B1 ; :: thesis: verum
end;
hence cB is axiom_UP3 ; :: thesis: verum