set S = { (square-uparrow n) where n is Nat : verum } ;
{ (square-uparrow n) where n is Nat : verum } c= bool [:NAT,NAT:]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (square-uparrow n) where n is Nat : verum } or x in bool [:NAT,NAT:] )
assume x in { (square-uparrow n) where n is Nat : verum } ; :: thesis: x in bool [:NAT,NAT:]
then ex n being Nat st x = square-uparrow n ;
hence x in bool [:NAT,NAT:] ; :: thesis: verum
end;
then reconsider S = { (square-uparrow n) where n is Nat : verum } as Subset-Family of [:NAT,NAT:] ;
now :: thesis: ( S is with_non-empty_elements & not S is empty & S is quasi_basis )
thus S is with_non-empty_elements :: thesis: ( not S is empty & S is quasi_basis )
proof
assume not S is with_non-empty_elements ; :: thesis: contradiction
then {} in S by SETFAM_1:def 8;
then ex n being Nat st {} = square-uparrow n ;
hence contradiction ; :: thesis: verum
end;
A1: square-uparrow 1 in S ;
hence not S is empty ; :: thesis: S is quasi_basis
thus S is quasi_basis :: thesis: verum
proof
let b1, b2 be Element of S; :: according to CARDFIL2:def 11 :: thesis: ex b1 being Element of S st b1 c= b1 /\ b2
b1 in S by A1;
then consider i being Nat such that
A2: b1 = square-uparrow i ;
b2 in S by A1;
then consider j being Nat such that
A3: b2 = square-uparrow j ;
reconsider i = i, j = j as Element of NAT by ORDINAL1:def 12;
reconsider n = max (i,j) as Element of NAT ;
square-uparrow n in S ;
hence ex b1 being Element of S st b1 c= b1 /\ b2 by A2, A3, Th29; :: thesis: verum
end;
end;
hence { (square-uparrow n) where n is Nat : verum } is filter_base of [:NAT,NAT:] ; :: thesis: verum