set X = { (NIC (i,l)) where l is Nat : verum } ;
{ (NIC (i,l)) where l is Nat : verum } c= bool NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (NIC (i,l)) where l is Nat : verum } or x in bool NAT )
assume x in { (NIC (i,l)) where l is Nat : verum } ; :: thesis: x in bool NAT
then ex l being Nat st x = NIC (i,l) ;
hence x in bool NAT ; :: thesis: verum

end;

then reconsider X = { (NIC (i,l)) where l is Nat : verum } as Subset-Family of NAT ;
meet X c= NAT ;
hence meet { (NIC (i,l)) where l is Nat : verum } is Subset of NAT ; :: thesis: verum