set S = { (square-uparrow n) where n is Nat : verum } ;

{ (square-uparrow n) where n is Nat : verum } c= bool [:NAT,NAT:]

{ (square-uparrow n) where n is Nat : verum } c= bool [:NAT,NAT:]

proof

then reconsider S = { (square-uparrow n) where n is Nat : verum } as Subset-Family of [:NAT,NAT:] ;
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;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

now :: thesis: ( S is with_non-empty_elements & not S is empty & S is quasi_basis )

hence
{ (square-uparrow n) where n is Nat : verum } is filter_base of [:NAT,NAT:]
; :: thesis: verumthus
S is with_non-empty_elements
:: thesis: ( not S is empty & S is quasi_basis )

hence not S is empty ; :: thesis: S is quasi_basis

thus S is quasi_basis :: thesis: verum

end;proof

A1:
square-uparrow 1 in S
;
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;then {} in S by SETFAM_1:def 8;

then ex n being Nat st {} = square-uparrow n ;

hence contradiction ; :: thesis: verum

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 b_{1} being Element of S st b_{1} 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 b_{1} being Element of S st b_{1} c= b1 /\ b2
by A2, A3, Th29; :: thesis: verum

end;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 b