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

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

meet X c= NAT ;

hence meet { (NIC (i,l)) where l is Nat : verum } is Subset of NAT ; :: thesis: verum

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

proof

then reconsider X = { (NIC (i,l)) where l is Nat : verum } as Subset-Family of NAT ;
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;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

meet X c= NAT ;

hence meet { (NIC (i,l)) where l is Nat : verum } is Subset of NAT ; :: thesis: verum